Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Primitive

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Documentation

type Pred a = a -> Bool Source #

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

type Fun a = a -> a Source #

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

class FromTerm a where Source #

Instances

Instances details
FromTerm Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Double Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

(ToTerm a, FromTerm a) => FromTerm [a] Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

class ToTerm a where Source #

Minimal complete definition

toTerm

Methods

toTerm :: TCM (a -> Term) Source #

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

Instances

Instances details
ToTerm Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Double Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm a => ToTerm [a] Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM ([a] -> Term) Source #

toTermR :: TCM ([a] -> ReduceM Term) Source #

(ToTerm a, ToTerm b) => ToTerm (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM ((a, b) -> Term) Source #

toTermR :: TCM ((a, b) -> ReduceM Term) Source #

class PrimTerm a where Source #

Methods

primTerm :: a -> TCM Term Source #

Instances

Instances details
PrimTerm Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Bool -> TCM Term Source #

PrimTerm Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Char -> TCM Term Source #

PrimTerm Double Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Str Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Str -> TCM Term Source #

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term Source #

PrimTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term Source #

PrimTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Lvl -> TCM Term Source #

PrimTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term Source #

PrimTerm a => PrimTerm [a] Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: [a] -> TCM Term Source #

PrimTerm a => PrimTerm (IO a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: IO a -> TCM Term Source #

(PrimType a, PrimType b) => PrimTerm (a -> b) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: (a -> b) -> TCM Term Source #

(PrimType a, PrimType b) => PrimTerm (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: (a, b) -> TCM Term Source #

class PrimType a where Source #

Methods

primType :: a -> TCM Type Source #

Instances

Instances details
PrimTerm a => PrimType a Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: a -> TCM Type Source #

newtype Lvl Source #

Constructors

Lvl 

Fields

Instances

Instances details
Eq Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: Lvl -> Lvl -> Bool #

(/=) :: Lvl -> Lvl -> Bool #

Ord Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

compare :: Lvl -> Lvl -> Ordering #

(<) :: Lvl -> Lvl -> Bool #

(<=) :: Lvl -> Lvl -> Bool #

(>) :: Lvl -> Lvl -> Bool #

(>=) :: Lvl -> Lvl -> Bool #

max :: Lvl -> Lvl -> Lvl #

min :: Lvl -> Lvl -> Lvl #

Show Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Lvl -> ShowS #

show :: Lvl -> String #

showList :: [Lvl] -> ShowS #

FromTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Lvl -> TCM Term Source #

newtype Nat Source #

Constructors

Nat 

Fields

Instances

Instances details
Enum Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

succ :: Nat -> Nat #

pred :: Nat -> Nat #

toEnum :: Int -> Nat #

fromEnum :: Nat -> Int #

enumFrom :: Nat -> [Nat] #

enumFromThen :: Nat -> Nat -> [Nat] #

enumFromTo :: Nat -> Nat -> [Nat] #

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #

Eq Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: Nat -> Nat -> Bool #

(/=) :: Nat -> Nat -> Bool #

Integral Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

quot :: Nat -> Nat -> Nat #

rem :: Nat -> Nat -> Nat #

div :: Nat -> Nat -> Nat #

mod :: Nat -> Nat -> Nat #

quotRem :: Nat -> Nat -> (Nat, Nat) #

divMod :: Nat -> Nat -> (Nat, Nat) #

toInteger :: Nat -> Integer #

Num Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

compare :: Nat -> Nat -> Ordering #

(<) :: Nat -> Nat -> Bool #

(<=) :: Nat -> Nat -> Bool #

(>) :: Nat -> Nat -> Bool #

(>=) :: Nat -> Nat -> Bool #

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Real Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toRational :: Nat -> Rational #

Show Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

TermLike Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat Source #

foldTerm :: Monoid m => (Term -> m) -> Nat -> m Source #

FromTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term 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.

mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl Source #

mkPrimInjective takes two Set0 a and b and a function f of type a -> b and outputs a primitive internalizing the fact that f is injective.

primEraseEquality :: TCM PrimitiveImpl Source #

primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y

getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo) Source #

Get the ArgInfo of the principal argument of BUILTIN REFL.

Returns Nothing for e.g. data Eq {a} {A : Set a} (x : A) : A → Set a where refl : Eq x x

Returns Just ... for e.g. data Eq {a} {A : Set a} : (x y : A) → Set a where refl : ∀ x → Eq x x

genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl Source #

Used for both primForce and primForceLemma.

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 #