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

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.IApplyConfluence

Synopsis

checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence :: QName -> Closure Clause -> TCM ()

Documentation

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.