ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Internal.SanityCheck
Sanity checking for internal syntax. Mostly checking variable scoping.
Synopsis
- value sanityCheckVars
- value sanityCheckSubst
- PackageAgda-2.8.0.2
- Exports2
- LanguageHaskell2010
- LicenceMIT
- SourceSanityCheck.hs
Check that Γ ⊢ ρ : Δ.