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

newtype Nat Source #

Constructors

Nat 

Fields

Instances

Instances details
Pretty Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Nat -> Doc Source #

prettyPrec :: Int -> Nat -> Doc Source #

prettyList :: [Nat] -> Doc Source #

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 Pred a = a -> Bool Source #

type Fun a = a -> a Source #

primEraseEquality :: TCM PrimitiveImpl Source #

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

newtype Lvl Source #

Constructors

Lvl 

Fields

Instances

Instances details
Pretty Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Lvl -> Doc Source #

prettyPrec :: Int -> Lvl -> Doc Source #

prettyList :: [Lvl] -> Doc Source #

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

Methods

primType :: Word64 -> TCM Type Source #

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

Methods

primType :: Integer -> TCM Type Source #

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

Methods

primType :: Double -> TCM Type Source #

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

Methods

primTerm :: Word64 -> TCM Term Source #

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

Methods

primTerm :: Integer -> TCM Term Source #

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

Methods

primTerm :: Double -> TCM Term Source #

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

Methods

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

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

ToTerm Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

ToTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

ToTerm Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

ToTerm Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

ToTerm Double Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

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 #

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

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

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

Methods

fromTerm :: TCM (FromTermFunction Word64) Source #

FromTerm Text Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Integer Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Integer) Source #

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

Methods

fromTerm :: TCM (FromTermFunction Double) Source #

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

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.

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

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 #

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