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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.IApplyConfluence

Synopsis

Documentation

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

addClause 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 the meta's MetaInfo and the context extension Δ is taken from the Closure.