ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Primitive

Primitive functions, such as addition on builtin integers.

7 types
4 classes
28 values

PackageAgda-2.7.0.1
Exports39
LanguageHaskell2010
LicenceMIT
SourcePrimitive.hs

module Agda.TypeChecking.Primitive.Base

module Agda.TypeChecking.Primitive.Cubical

newtypenewtype Nat

Constructors

Nat
- unNat :: Integer

Instances12Enum, Eq, Integral, Num, Ord, Real, …

Enum NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Eq NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Integral NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Num NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Ord NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Real NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Pretty NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
TermLike NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

valuegetRefl :: TCM (Arg Term -> Term)

valueprimitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)

typetype Pred a = a -> Bool

typetype Fun a = a -> a

valueprimWord64ToNatInjective :: TCM PrimitiveImpl

valueprimFloatToWord64Injective :: TCM PrimitiveImpl

valueprimCharToNatInjective :: TCM PrimitiveImpl

valueprimStringToListInjective :: TCM PrimitiveImpl

valueprimStringFromListInjective :: TCM PrimitiveImpl

valueprimEraseEquality :: TCM PrimitiveImpl

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

valueprimForce :: TCM PrimitiveImpl

valueprimForceLemma :: TCM PrimitiveImpl

valueprimQNameToWord64sInjective :: TCM PrimitiveImpl

valueprimMetaToNatInjective :: TCM PrimitiveImpl

newtypenewtype Lvl

Constructors

Lvl
- unLvl :: Integer

Instances7Eq, Ord, Pretty, FromTerm, PrimTerm, PrimType, …

Eq LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Ord LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
Pretty LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

classclass PrimType a where

Methods

primType :: a -> TCM Type

Instances17PrimType, …

PrimType QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType Fixity'Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType IntegerDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType Word64Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType BoolDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType CharDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType DoubleDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimType TextDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimType (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimType (IO a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimType [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(PrimType a, PrimType b) => PrimType (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(PrimType a, PrimType b) => PrimType (a -> b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

classclass PrimType a => PrimTerm a where

Methods

primTerm :: a -> TCM Term

Instances17PrimTerm, …

PrimTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm Fixity'Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm IntegerDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm Word64Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm BoolDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm CharDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm DoubleDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm TextDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimTerm (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimTerm (IO a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
PrimTerm a => PrimTerm [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(PrimType a, PrimType b) => PrimTerm (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(PrimType a, PrimType b) => PrimTerm (a -> b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

classclass ToTerm a where

Methods

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

Instances22ToTerm, …

ToTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm ArgInfoDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm AssociativityDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm FixityDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm Fixity'Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm FixityLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm BlockerDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm IntegerDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm Word64Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm BoolDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm CharDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm DoubleDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm TextDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm (Dom Type)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm a => ToTerm (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
ToTerm a => ToTerm [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(ToTerm a, ToTerm b) => ToTerm (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

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

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

typetype FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)

classclass FromTerm a where

Methods

fromTerm :: TCM (FromTermFunction a)

Instances12FromTerm, …

FromTerm QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm LvlDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm NatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm IntegerDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm Word64Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm BoolDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm CharDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm DoubleDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm TextDefined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
FromTerm a => FromTerm (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive
(ToTerm a, FromTerm a) => FromTerm [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Primitive

valuefromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)

valuefromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)

valuemkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl

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.

valuemetaToNat :: MetaId -> Nat

Converts MetaIds to natural numbers.

valuegetReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)

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

valuegenPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl

Used for both primForce and primForceLemma.

valuemkPrimLevelZero :: TCM PrimitiveImpl

valuemkPrimLevelSuc :: TCM PrimitiveImpl

valuemkPrimLevelMax :: TCM PrimitiveImpl

typetype Op a = a -> a -> a

valueprimLockUniv' :: TCM PrimitiveImpl

valuemkPrimFun1TCM

:: (FromTerm a, ToTerm b)
=> TCM Type
-> a -> ReduceM b
-> TCM PrimitiveImpl

valuemkPrimFun1

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

valuemkPrimFun2

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

valuemkPrimFun3

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

valuemkPrimFun4

:: (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

typetype Rel a = a -> a -> Bool