| 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.
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.