Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Primitive.Base

Synopsis

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 #

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

elInf :: Functor m => m Term -> m Type 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 #

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

tset :: Monad tcm => tcm Type 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

Builtin Sigma

data SigmaKit Source #

Constructors

SigmaKit 

Instances

Instances details
Eq SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Base

Show SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Base