Agda-2.8.0: 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

- (-->) :: 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' :: forall (m :: Type -> Type). (MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
- nPi' :: forall (m :: Type -> Type). (MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type
- pPi' :: forall (m :: Type -> Type). (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 :: forall (m :: Type -> Type). 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' :: forall (m :: Type -> Type). (MonadAddContext m, MonadDebug m) => String -> NamesT m Type -> (NamesT m Term -> NamesT m Type) -> NamesT m Type Source #

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

pPi' :: forall (m :: Type -> Type). (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 :: forall (m :: Type -> Type). 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 Source # show :: SigmaKit -> String Source # showList :: [SigmaKit] -> ShowS Source #
Eq SigmaKit Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Base Methods (==) :: SigmaKit -> SigmaKit -> Bool Source # (/=) :: SigmaKit -> SigmaKit -> Bool Source #

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