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

Safe Haskell	Safe-Inferred
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 ()

Documentation

sanityCheckVars :: (Pretty a, Free a) => Telescope -> a -> TCM () Source #

sanityCheckSubst :: (Pretty a, Free a) => Telescope -> Substitution' a -> Telescope -> TCM () Source #

Check that Γ ⊢ ρ : Δ.