Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





class (Functor m, Applicative m, Monad m) => HasBuiltins m where Source #

Minimal complete definition


constructorForm :: Term -> TCM Term Source #

Rewrite a literal to constructor form if possible.

The names of built-in things

builtinsNoDef :: [String] Source #

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.


The type of Type would be Type : Level → Setω which is not valid Agda.

data CoinductionKit Source #

The coinductive primitives.

Builtin equality

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type Source #

Revert the EqualityView.

Postcondition: type is reduced.