| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Rules.Builtin

Contents

Checking builtin pragmas

Synopsis

builtinDatatypes :: [(String, Int)]
inductiveCheck :: String -> Term -> TCM ()
bindBuiltinType :: String -> Expr -> TCM ()
bindBuiltinBool :: String -> Expr -> TCM ()
bindBuiltinType1 :: String -> Expr -> TCM ()
bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM ()
bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM ()
typeOfSizeInf :: TCM Type
typeOfSizeSuc :: TCM Type
bindBuiltinNil :: Expr -> TCM ()
bindBuiltinCons :: Expr -> TCM ()
bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM ()
builtinPrimitives :: [(String, (String, Term -> TCM ()))]
bindBuiltinEquality :: Expr -> TCM ()
bindBuiltinRefl :: Expr -> TCM ()
builtinConstructors :: [(String, Expr -> TCM ())]
builtinPostulates :: [(String, TCM Type)]
bindConstructor :: String -> (Expr -> TCM ()) -> Expr -> TCM ()
bindPostulate :: String -> TCM Type -> Expr -> TCM ()
bindBuiltin :: String -> Expr -> TCM ()

Checking builtin pragmas

builtinDatatypes :: [(String, Int)] | Source

inductiveCheck :: String -> Term -> TCM () | Source

bindBuiltinType :: String -> Expr -> TCM () | Source

bindBuiltinBool :: String -> Expr -> TCM () | Source

bindBuiltinType1 :: String -> Expr -> TCM () | Source

Bind something of type `Set -> Set`.

bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM () | Source

bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM () | Source

typeOfSizeInf :: TCM Type | Source

typeOfSizeSuc :: TCM Type | Source

bindBuiltinNil :: Expr -> TCM () | Source

Built-in nil should have type `{A:Set} -> List A`

bindBuiltinCons :: Expr -> TCM () | Source

Built-in cons should have type `{A:Set} -> A -> List A -> List A`

bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM () | Source

builtinPrimitives :: [(String, (String, Term -> TCM ()))] | Source

bindBuiltinEquality :: Expr -> TCM () | Source

bindBuiltinRefl :: Expr -> TCM () | Source

builtinConstructors :: [(String, Expr -> TCM ())] | Source

Builtin constructors

builtinPostulates :: [(String, TCM Type)] | Source

Builtin postulates

bindConstructor :: String -> (Expr -> TCM ()) -> Expr -> TCM () | Source

Bind a builtin constructor. Pre-condition: argument is an element of `builtinConstructors`.

bindPostulate :: String -> TCM Type -> Expr -> TCM () | Source

Bind a builtin postulate. Pre-condition: argument is an element of `builtinPostulates`.

bindBuiltin :: String -> Expr -> TCM () | Source

Bind a builtin thing to an expression.
Produced by Haddock version 2.4.2