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

Documentation

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

Minimal complete definition

getBuiltinThing

Methods

Instances

 MonadIO m => HasBuiltins (TCMT m) Source # Methods

Rewrite a literal to constructor form if possible.

The names of built-in things

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.

The coinductive primitives.

Constructors

 CoinductionKit FieldsnameOfInf :: QName nameOfSharp :: QName nameOfFlat :: QName

Tries to build a CoinductionKit.

Builtin equality

Get the name of the equality type.

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

Precondition: type is reduced.

Revert the EqualityView.

Postcondition: type is reduced.