Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Primitive.Base

Synopsis

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 #

el' :: Applicative m => m Term -> 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 #

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 #

el :: Functor m => m Term -> 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

Builtin Sigma

data SigmaKit Source #

Constructors

SigmaKit 

Instances

Instances details
Show SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Base

Eq SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Base