ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.IApplyConfluence
- 4 values
- PackageAgda-2.7.0.1
- Exports4
- LanguageHaskell2010
- LicenceMIT
- SourceIApplyConfluence.hs
checkIApplyConfluence f (Clause {namedClausePats = ps}) checks that f ps
reduces in a way that agrees with IApply reductions.
value
unifyElims current context is of the form Γ.Δ
Like unifyElims but Γ is from the meta's MetaInfo and
the context extension Δ is taken from the Closure.