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

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Lock

Documentation

isTimeless :: Type -> TCM Bool Source #

checkLockedVars Source #

Arguments

:: Term	term to check
-> Type	its type
-> Arg Term	the lock
-> Type	type of the lock
-> TCM ()

checkEarlierThan :: Term -> VarSet -> TCM () Source #

requireGuarded :: String -> TCM () Source #