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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Primitive

Contents

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Primitive functions

newtype Nat

Constructors

Nat 

Fields

unNat :: Integer
 

newtype Lvl

Constructors

Lvl 

Fields

unLvl :: Integer
 

class PrimType a where

Methods

primType :: a -> TCM Type

Instances

class ToTerm a where

Minimal complete definition

toTerm

Methods

toTerm :: TCM (a -> Term)

toTermR :: TCM (a -> ReduceM Term)

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

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

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

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

redReturn :: a -> ReduceM (Reduced a' a)

mkPrimFun2 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, PrimType c, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImpl

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

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

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

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

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

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

argN :: e -> Arg e

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom e

argH :: e -> Arg e

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom e

The actual primitive functions

type Op a = a -> a -> a

type Fun a = a -> a

type Rel a = a -> a -> Bool

type Pred a = a -> Bool