- builtinDatatypes :: [(String, Int)]
- inductiveCheck :: String -> Term -> TCM ()
- bindBuiltinType :: String -> Expr -> TCM ()
- bindBuiltinBool :: String -> Expr -> TCM Term
- bindBuiltinType1 :: String -> Expr -> TCM ()
- bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM Term
- bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM Term
- typeOfSizeInf :: TCM Type
- typeOfSizeSuc :: TCM Type
- bindBuiltinNil :: Expr -> TCM Term
- bindBuiltinCons :: Expr -> TCM Term
- bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM ()
- builtinPrimitives :: [(String, (String, Term -> TCM ()))]
- bindBuiltinEquality :: Expr -> TCM ()
- bindBuiltinRefl :: Expr -> TCM Term
- bindBuiltinDummyConstructor :: Expr -> TCM Term
- bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()
- builtinConstructors :: [(String, Expr -> TCM Term)]
- builtinPostulates :: [(String, TCM Type)]
- bindConstructor :: String -> (Expr -> TCM Term) -> Expr -> TCM ()
- bindPostulate :: String -> TCM Type -> Expr -> TCM ()
- bindBuiltin :: String -> Expr -> TCM ()
Checking builtin pragmas
builtinDatatypes :: [(String, Int)]Source
bindBuiltinNil :: Expr -> TCM TermSource
Built-in nil should have type {A:Set} -> List A
bindBuiltinCons :: Expr -> TCM TermSource
Built-in cons should have type {A:Set} -> A -> List A -> List A
bindBuiltinEquality :: Expr -> TCM ()Source
bindBuiltinRefl :: Expr -> TCM TermSource
bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()Source
bindPostulatedName builtin e m
checks that e
is a postulated
name q
, and binds the builtin builtin
to the term m q def
,
where def
is the current Definition
of q
.
builtinPostulates :: [(String, TCM Type)]Source
Builtin postulates
bindConstructor :: String -> (Expr -> TCM Term) -> 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
.