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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Rules.Builtin

Synopsis

- bindBuiltin :: String -> ResolvedName -> TCM ()
- bindBuiltinNoDef :: String -> QName -> TCM ()
- builtinKindOfName :: String -> Maybe KindOfName
- bindPostulatedName :: String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
- isUntypedBuiltin :: String -> Bool
- bindUntypedBuiltin :: String -> ResolvedName -> TCM ()

# Documentation

bindBuiltin :: String -> ResolvedName -> TCM () Source #

Bind a builtin thing to an expression.

bindBuiltinNoDef :: String -> QName -> TCM () Source #

Bind a builtin thing to a new name.

Since their type is closed, it does not matter whether we are in a parameterized module when we declare them. We simply ignore the parameters.

builtinKindOfName :: String -> Maybe KindOfName Source #

bindPostulatedName :: String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM () Source #

`bindPostulatedName builtin q m` checks that `q` is a postulated name, and binds the builtin `builtin` to the term `m q def`, where `def` is the current `Definition` of `q`.

isUntypedBuiltin :: String -> Bool Source #

bindUntypedBuiltin :: String -> ResolvedName -> TCM () Source #