Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.IApplyConfluence

Synopsis

- checkIApplyConfluence_ :: QName -> TCM ()
- checkIApplyConfluence :: QName -> Clause -> TCM ()
- unifyElims :: Args -> Args -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
- unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term, Term)] -> Constraint -> TCM a) -> TCM a

# Documentation

checkIApplyConfluence_ :: QName -> TCM () Source #

checkIApplyConfluence :: QName -> Clause -> TCM () Source #

`checkIApplyConfluence f (Clause {namedClausePats = ps})` checks that `f ps` reduces in a way that agrees with `IApply` reductions.

unifyElims Source #

Arguments

:: Args | variables to keep Γ ⊢ x_n .. x_0 : Γ
-> Args | variables to solve Γ.Δ ⊢ ts : Γ
-> (Substitution -> [(Term, Term)] -> TCM a) |
-> TCM a |

current context is of the form Γ.Δ

unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term, Term)] -> Constraint -> TCM a) -> TCM a Source #

Like `unifyElims` but `Γ` is from the meta's `MetaInfo` and the context extension `Δ` is taken from the `Closure`.