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

Safe HaskellSafe
LanguageHaskell2010

Agda.Syntax.Builtin

Description

This module defines the names of all BUILTINs.

Synopsis

Documentation

builtinNat :: String Source #

builtinSuc :: String Source #

builtinZero :: String Source #

builtinChar :: String Source #

builtinUnit :: String Source #

builtinBool :: String Source #

builtinTrue :: String Source #

builtinList :: String Source #

builtinNil :: String Source #

builtinCons :: String Source #

builtinIO :: String Source #

builtinPath :: String Source #

builtinIOne :: String Source #

builtinIMin :: String Source #

builtinIMax :: String Source #

builtinINeg :: String Source #

builtinComp :: String Source #

builtinPOr :: String Source #

builtinSub :: String Source #

builtinGlue :: String Source #

builtinId :: String Source #

builtinSize :: String Source #

builtinInf :: String Source #

builtinFlat :: String Source #

builtinRefl :: String Source #

builtinArg :: String Source #

builtinAbs :: String Source #

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.

sizeBuiltins :: [String] Source #