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

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Lock

Synopsis

isTimeless :: Type -> TCM Bool
checkLockedVars :: Term -> Type -> Arg Term -> Type -> TCM ()
checkEarlierThan :: Term -> VarSet -> TCM Bool

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 Bool Source #

If the first argument is a lock variable, check that all variables in the given set are either earlier than this variable or are timeless.