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.