| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal.SanityCheck
Description
Sanity checking for internal syntax. Mostly checking variable scoping.
Synopsis
- sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM ()
- sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM ()