Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Primitive

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Documentation

newtype Nat Source #

Constructors

Nat 

Fields

Instances

Instances details
Pretty Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

PrimTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term Source #

PrimType Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Nat -> TCM Type Source #

ToTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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] #

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 #

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 #

Real Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toRational :: Nat -> Rational #

Eq Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

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 #

type Fun a = a -> a Source #

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

type Pred a = a -> Bool Source #

newtype Lvl Source #

Constructors

Lvl 

Fields

Instances

Instances details
Pretty Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm 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 #

PrimType Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Lvl -> TCM Type Source #

ToTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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 #

class PrimType a where Source #

Minimal complete definition

Nothing

Methods

primType :: a -> TCM Type Source #

default primType :: PrimTerm a => a -> TCM Type Source #

Instances

Instances details
PrimType QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: QName -> TCM Type Source #

PrimType Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Type -> TCM Type Source #

PrimType Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Lvl -> TCM Type Source #

PrimType Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Nat -> TCM Type Source #

PrimType Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Text -> TCM Type Source #

PrimType Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimType Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Bool -> TCM Type Source #

PrimType Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Char -> TCM Type Source #

PrimType Double Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.TypeChecking.Primitive

Methods

primType :: IO a -> TCM Type Source #

PrimTerm a => PrimType (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Maybe a -> TCM Type Source #

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

Defined in Agda.TypeChecking.Primitive

Methods

primType :: [a] -> TCM Type Source #

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

Defined in Agda.TypeChecking.Primitive

Methods

primType :: (a, b) -> TCM Type Source #

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

Defined in Agda.TypeChecking.Primitive

Methods

primType :: (a -> b) -> TCM Type Source #

class PrimType a => PrimTerm a where Source #

Methods

primTerm :: a -> TCM Term Source #

Instances

Instances details
PrimTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term Source #

PrimTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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 Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Text -> TCM Term Source #

PrimTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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 a => PrimTerm (IO a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: IO a -> TCM Term Source #

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

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Maybe a -> TCM Term Source #

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

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: [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 ToTerm a where Source #

Minimal complete definition

toTerm

Methods

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

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

Instances

Instances details
ToTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Associativity 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 FixityLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Blocker 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 Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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 (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm a => ToTerm (Maybe a) 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 FromTerm a where Source #

Instances

Instances details
FromTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm MetaId 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

FromTerm Word64 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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 a => FromTerm (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

Defined in Agda.TypeChecking.Primitive

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

primEraseEquality :: TCM PrimitiveImpl Source #

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

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.

metaToNat :: MetaId -> Nat Source #

Converts MetaIds to natural numbers.

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.

mkPrimFun3 :: (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 Source #

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 #