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

Agda.TypeChecking.Primitive

Description

Primitive functions, such as addition on builtin integers.

Synopsis

# Primitive functions

Constructors

 PrimImpl Type PrimFun

newtype Nat Source

Constructors

 Nat FieldsunNat :: Integer

Instances

 Source Source Source Source Source Source Source Source Source Source

newtype Lvl Source

Constructors

 Lvl FieldsunLvl :: Integer

Instances

 Source Source Source Source Source Source

class PrimType a where Source

Methods

primType :: a -> TCM Type Source

Instances

 PrimTerm a => PrimType a Source

class PrimTerm a where Source

Methods

primTerm :: a -> TCM Term Source

Instances

 Source Source Source Source Source Source Source Source Source PrimTerm a => PrimTerm [a] Source PrimTerm a => PrimTerm (IO a) Source (PrimType a, PrimType b) => PrimTerm (a -> b) Source

class ToTerm a where Source

Minimal complete definition

toTerm

Methods

toTerm :: TCM (a -> Term) Source

toTermR :: TCM (a -> ReduceM Term) Source

Instances

 Source Source Source Source Source Source Source Source Source Source Source (PrimTerm a, ToTerm a) => ToTerm [a] Source

buildList :: TCM ([Term] -> Term) Source

`buildList A ts` builds a list of type `List A`. Assumes that the terms `ts` all have type `A`.

class FromTerm a where Source

Methods

Instances

 Source Source Source Source Source Source Source Source (ToTerm a, FromTerm a) => FromTerm [a] Source

redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') Source

Conceptually: `redBind m f k = either (return . Left . f) k =<< m`

mkPrimFun4 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d, PrimType e, ToTerm e) => (a -> b -> c -> d -> e) -> TCM PrimitiveImpl Source

(-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 Source

(.-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 Source

(..-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 Source

(<@>) :: TCM Term -> TCM Term -> TCM Term infixl 9 Source

(<#>) :: TCM Term -> TCM Term -> TCM Term infixl 9 Source

argN :: e -> Arg e Source

Abbreviation: `argN = Arg defaultArgInfo`.

domN :: e -> Dom e Source

argH :: e -> Arg e Source

Abbreviation: `argH = hide Arg defaultArgInfo`.

domH :: e -> Dom e Source

# The actual primitive functions

type Op a = a -> a -> a Source

type Fun a = a -> a Source

type Rel a = a -> a -> Bool Source

type Pred a = a -> Bool Source