Agda-2.6.3.20230930: 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 #

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 #

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 #

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

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

Convert a name in Term form back to QName.

Builtin Sigma

data SigmaKit Source #

Constructors

SigmaKit 

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