Agda-2.6.0: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.IApplyConfluence
checkIApplyConfluence_ :: QName -> TCM () Source #
checkIApplyConfluence :: QName -> Closure Clause -> TCM () Source #
addClause f (Clause {namedClausePats = ps}) checks that f ps reduces in a way that agrees with IApply reductions.
addClause f (Clause {namedClausePats = ps})
f ps
IApply