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

Safe Haskell | Safe-Inferred
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 #