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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Builtin

Contents

Synopsis

Documentation

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

constructorForm :: Term -> TCM Term

Rewrite a literal to constructor form if possible.

The names of built-in things

data CoinductionKit

The coinductive primitives.

Builtin equality

primEqualityName :: TCM QName

Get the name of the equality type.