Agda-2.7.0: A dependently typed functional programming language and proof assistant

Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Primitive.Base

Contents

Accessing the primitive functions
Builtin Sigma

Synopsis

(-->) :: Applicative m => m Type -> m Type -> m Type
(.-->) :: Applicative m => m Type -> m Type -> m Type
(..-->) :: Applicative m => m Type -> m Type -> m Type
garr :: Applicative m => (Relevance -> Relevance) -> m Type -> m Type -> m Type
gpi :: (MonadAddContext m, MonadDebug m) => ArgInfo -> String -> m Type -> m Type -> m Type
hPi :: (MonadAddContext m, MonadDebug m) => String -> m Type -> m Type -> m Type
nPi :: (MonadAddContext m, MonadDebug m) => String -> m Type -> m Type -> m Type
hPi' :: (MonadFail m, MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
nPi' :: (MonadFail m, MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m) => String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
toFinitePi :: Type -> Type
el' :: Applicative m => m Term -> m Term -> m Type
els :: Applicative m => m Sort -> m Term -> m Type
el's :: Applicative m => m Term -> m Term -> m Type
elInf :: Functor m => m Term -> m Type
elSSet :: Functor m => m Term -> m Type
nolam :: Term -> Term
varM :: Applicative m => Int -> m Term
gApply :: Applicative m => Hiding -> m Term -> m Term -> m Term
gApply' :: Applicative m => ArgInfo -> m Term -> m Term -> m Term
(<@>) :: Applicative m => m Term -> m Term -> m Term
(<#>) :: Applicative m => m Term -> m Term -> m Term
(<..>) :: Applicative m => m Term -> m Term -> m Term
(<@@>) :: Applicative m => m Term -> (m Term, m Term, m Term) -> m Term
list :: TCM Term -> TCM Term
tMaybe :: TCM Term -> TCM Term
io :: TCM Term -> TCM Term
path :: TCM Term -> TCM Term
el :: Functor m => m Term -> m Type
tset :: Applicative m => m Type
sSizeUniv :: Sort
tSizeUniv :: Applicative m => m Type
tLevelUniv :: Applicative m => m Type
argN :: e -> Arg e
domN :: e -> Dom e
argH :: e -> Arg e
domH :: e -> Dom e
lookupPrimitiveFunction :: PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl)
getBuiltinName :: (HasBuiltins m, MonadReduce m) => BuiltinId -> m (Maybe QName)
getQNameFromTerm :: MonadReduce m => Term -> MaybeT m QName
isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> BuiltinId -> m Bool
data SigmaKit = SigmaKit {
- sigmaName :: QName
- sigmaCon :: ConHead
- sigmaFst :: QName
- sigmaSnd :: QName
}
getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)

Documentation

(-->) :: Applicative m => m Type -> m Type -> m Type infixr 4 Source #

(.-->) :: Applicative m => m Type -> m Type -> m Type infixr 4 Source #

(..-->) :: Applicative m => m Type -> m Type -> m Type infixr 4 Source #

garr :: Applicative m => (Relevance -> Relevance) -> m Type -> m Type -> m Type Source #

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

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

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

hPi' :: (MonadFail m, MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type Source #

nPi' :: (MonadFail m, MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type Source #

pPi' :: (MonadAddContext m, HasBuiltins m, MonadDebug m) => String -> NamesT m Term -> (NamesT m Term -> NamesT m Type) -> NamesT m Type Source #

toFinitePi :: 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.

el' :: Applicative m => m Term -> m Term -> m Type Source #

els :: Applicative m => m Sort -> m Term -> m Type Source #

el's :: Applicative m => m Term -> m Term -> m Type Source #

elInf :: Functor m => m Term -> m Type Source #

elSSet :: Functor m => m Term -> m Type Source #

nolam :: Term -> Term Source #

varM :: Applicative m => Int -> m Term Source #

gApply :: Applicative m => Hiding -> m Term -> m Term -> m Term Source #

gApply' :: Applicative m => ArgInfo -> m Term -> m Term -> m Term Source #

(<@>) :: Applicative m => m Term -> m Term -> m Term infixl 9 Source #

(<#>) :: Applicative m => m Term -> m Term -> m Term infixl 9 Source #

(<..>) :: Applicative m => m Term -> m Term -> m Term Source #

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

list :: TCM Term -> TCM Term Source #

tMaybe :: TCM Term -> TCM Term Source #

io :: TCM Term -> TCM Term Source #

path :: TCM Term -> TCM Term Source #

el :: Functor m => m Term -> m Type Source #

tset :: Applicative m => m Type Source #

The universe Set0 as a type.

sSizeUniv :: Sort Source #

SizeUniv as a sort.

tSizeUniv :: Applicative m => m Type Source #

SizeUniv as a type.

tLevelUniv :: Applicative m => m Type Source #

argN :: e -> Arg e Source #

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom e Source #

argH :: e -> Arg e Source #

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom e Source #

Accessing the primitive functions

lookupPrimitiveFunction :: PrimitiveId -> TCM PrimitiveImpl Source #

lookupPrimitiveFunctionQ :: QName -> TCM (PrimitiveId, PrimitiveImpl) Source #

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

getQNameFromTerm :: MonadReduce m => Term -> MaybeT m QName Source #

Convert a name in Term form back to QName.

isBuiltin :: (HasBuiltins m, MonadReduce m) => QName -> BuiltinId -> m Bool Source #

Builtin Sigma

data SigmaKit Source #

Constructors

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

Instances

Instances details

Show SigmaKit Source #
Instance details Defined in Agda.TypeChecking.Primitive.Base Methods showsPrec :: Int -> SigmaKit -> ShowS # show :: SigmaKit -> String # showList :: [SigmaKit] -> ShowS #
Eq SigmaKit Source #
Instance details Defined in Agda.TypeChecking.Primitive.Base Methods (==) :: SigmaKit -> SigmaKit -> Bool # (/=) :: SigmaKit -> SigmaKit -> Bool #

getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit) Source #