Agda-2.4.0.2: 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 Str

Constructors

Str 

Fields

unStr :: String
 

newtype Nat

Constructors

Nat 

Fields

unNat :: Integer
 

newtype Lvl

Constructors

Lvl 

Fields

unLvl :: Integer
 

class PrimType a where

Methods

primType :: a -> TCM Type

Instances

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, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, 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 Term -> TCM Term -> TCM Term infixl 9

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

argN :: e -> Arg c e

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom c e

argH :: e -> Arg c e

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom c 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