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

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Primitive.Base

Contents

Accessing the primitive functions
Builtin Sigma

Synopsis

(-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
(.-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
(..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
garr :: Monad 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
el' :: Monad m => m Term -> m Term -> m Type
elInf :: Functor m => m Term -> m Type
nolam :: Term -> Term
varM :: Monad tcm => Int -> tcm Term
gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term
gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term
(<@>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
(<#>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
(<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
(<@@>) :: Monad tcm => tcm Term -> (tcm Term, tcm Term, tcm Term) -> tcm Term
list :: TCM Term -> TCM Term
io :: TCM Term -> TCM Term
path :: TCM Term -> TCM Term
el :: Functor tcm => tcm Term -> tcm Type
tset :: Monad tcm => tcm Type
sSizeUniv :: Sort
tSizeUniv :: Monad tcm => tcm Type
argN :: e -> Arg e
domN :: e -> Dom e
argH :: e -> Arg e
domH :: e -> Dom e
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
getBuiltinName :: String -> TCM (Maybe QName)
isBuiltin :: QName -> String -> TCM Bool
data SigmaKit = SigmaKit {
- sigmaName :: QName
- sigmaCon :: ConHead
- sigmaFst :: QName
- sigmaSnd :: QName
}
getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)

Documentation

(-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

(.-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

(..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

garr :: Monad 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 #

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

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

nolam :: Term -> Term Source #

varM :: Monad tcm => Int -> tcm Term Source #

gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term Source #

gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term Source #

(<@>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term infixl 9 Source #

(<#>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term infixl 9 Source #

(<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term Source #

(<@@>) :: Monad tcm => tcm Term -> (tcm Term, tcm Term, tcm Term) -> tcm Term Source #

list :: TCM Term -> TCM Term Source #

io :: TCM Term -> TCM Term Source #

path :: TCM Term -> TCM Term Source #

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

tset :: Monad tcm => tcm Type Source #

sSizeUniv :: Sort Source #

tSizeUniv :: Monad tcm => tcm 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 :: String -> TCM PrimitiveImpl Source #

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

getBuiltinName :: String -> TCM (Maybe QName) Source #

isBuiltin :: QName -> String -> TCM Bool Source #

Builtin Sigma

data SigmaKit Source #

Constructors

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

Instances

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

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