ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Primitive.Base

1 type
43 values

PackageAgda-2.7.0.1
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'

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

valuenPi'

:: (MonadFail m, 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

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

The universe Set0 as a type.

valuesSizeUniv :: Sort

SizeUniv as a sort.

valuetSizeUniv :: Applicative m => m Type

SizeUniv as a type.

valuetLevelUniv :: Applicative m => m Type

valueargN :: e -> Arg e

Abbreviation: argN = Arg defaultArgInfo.

valuedomN :: e -> Dom e

valueargH :: e -> Arg e

Abbreviation: argH = hide Arg defaultArgInfo.

valuedomH :: e -> Dom e

Accessing the primitive functions

5 declarations

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

Convert a name in Term form back to QName.

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

Builtin Sigma

2 declarations

datadata SigmaKit

Constructors

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

Instances2Eq, Show

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

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