ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Primitive.Base

Contents

Accessing the primitive functions
Builtin Sigma

Synopsis

value -->
value .-->
value ..-->
value garr
value gpi
value hPi
value nPi
value hPi'
value nPi'
value pPi'
value toFinitePi
value el'
value els
value el's
value elInf
value elSSet
value nolam
value varM
value gApply
value gApply'
value <@>
value <#>
value <..>
value <@@>
value list
value tMaybe
value io
value path
value el
value tset
value sSizeUniv
value tSizeUniv
value tLevelUniv
value argN
value domN
value argH
value domH
value lookupPrimitiveFunction
value lookupPrimitiveFunctionQ
value getBuiltinName
value getQNameFromTerm
value isBuiltin
data SigmaKit
value getSigmaKit

PackageAgda-2.8.0.2
Exports44
LanguageHaskell2010
LicenceMIT
SourceBase.hs

value(-->) :: Applicative m => m Type -> m Type -> m Type

value(.-->) :: Applicative m => m Type -> m Type -> m Type

value(..-->) :: Applicative m => m Type -> m Type -> m Type

valuegarr

:: Applicative m
=> Relevance -> Relevance
-> m Type
-> m Type
-> m Type

valuegpi

:: (MonadAddContext m, MonadDebug m)
=> ArgInfo
-> String
-> m Type
-> m Type
-> m Type

valuehPi

:: (MonadAddContext m, MonadDebug m)
=> String
-> m Type
-> m Type
-> m Type

valuenPi

:: (MonadAddContext m, MonadDebug m)
=> String
-> m Type
-> m Type
-> m Type

valuehPi'

:: (MonadAddContext m, MonadDebug m)
=> String
-> NamesT m Type
-> NamesT m Term -> NamesT m Type
-> NamesT m Type

valuenPi'

:: (MonadAddContext m, MonadDebug m)
=> String
-> NamesT m Type
-> NamesT m Term -> NamesT m Type
-> NamesT m Type

valuepPi'

:: (MonadAddContext m, HasBuiltins m, MonadDebug m)
=> String
-> NamesT m Term
-> NamesT m Term -> NamesT m Type
-> NamesT m Type

valuetoFinitePi :: Type -> Type

Source#

Turn a Pi type into one whose domain is annotated finite, i.e., one that represents a Partial element rather than an actual function.

valueel' :: Applicative m => m Term -> m Term -> m Type

valueels :: Applicative m => m Sort -> m Term -> m Type

valueel's :: Applicative m => m Term -> m Term -> m Type

valueelInf :: Functor m => m Term -> m Type

valueelSSet :: Functor m => m Term -> m Type

valuenolam :: Term -> Term

valuevarM :: Applicative m => Int -> m Term

valuegApply :: Applicative m => Hiding -> m Term -> m Term -> m Term

valuegApply' :: Applicative m => ArgInfo -> m Term -> m Term -> m Term

value(<@>) :: Applicative m => m Term -> m Term -> m Term

value(<#>) :: Applicative m => m Term -> m Term -> m Term

value(<..>) :: Applicative m => m Term -> m Term -> m Term

value(<@@>) :: Applicative m => m Term -> (m Term, m Term, m Term) -> m Term

valuelist :: TCM Term -> TCM Term

valuetMaybe :: TCM Term -> TCM Term

valueio :: TCM Term -> TCM Term

valuepath :: TCM Term -> TCM Term

valueel :: Functor m => m Term -> m Type

valuetset :: Applicative m => m Type

Source#

The universe Set0 as a type.

valuesSizeUniv :: Sort

Source#

SizeUniv as a sort.

valuetSizeUniv :: Applicative m => m Type

Source#

SizeUniv as a type.

valuetLevelUniv :: Applicative m => m Type

valueargN :: e -> Arg e

Source#

Abbreviation: argN = Arg defaultArgInfo.

valuedomN :: e -> Dom e

valueargH :: e -> Arg e

Source#

Abbreviation: argH = hide Arg defaultArgInfo.

valuedomH :: e -> Dom e

Accessing the primitive functions

valuelookupPrimitiveFunction :: PrimitiveId -> TCM PrimitiveImpl

valuelookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl)

valuegetBuiltinName

:: (HasBuiltins m, MonadReduce m)
=> BuiltinId
-> m (Maybe QName)

valuegetQNameFromTerm :: MonadReduce m => Term -> MaybeT m QName

Source#

Convert a name in Term form back to QName.

valueisBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> BuiltinId -> m Bool

Builtin Sigma

datadata SigmaKit

Constructors

SigmaKit
- sigmaName :: QName
- sigmaCon :: ConHead
- sigmaFst :: QName
- sigmaSnd :: QName

Instances2Eq, Show

Eq SigmaKitDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Base
Show SigmaKitDefined in Agda-2.8.0.2 · Agda.TypeChecking.Primitive.Base

valuegetSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)