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.