Agda-2.4.2.5: 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

class PrimType a where Source

Methods

primType :: a -> TCM Type Source

Instances

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

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') 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