Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 #