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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

Documentation

data CoinductionKit Source #

The coinductive primitives.

class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where Source #

Methods

getBuiltinThing :: String -> m (Maybe (Builtin PrimFun)) Source #

Instances
HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun)) Source #

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> StateT s m (Maybe (Builtin PrimFun)) Source #

bindBuiltinName :: String -> Term -> TCM () Source #

bindPrimitive :: String -> PrimFun -> TCM () Source #

getBuiltin :: String -> TCM Term Source #

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term) Source #

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun) Source #

getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term) Source #

getTerm' :: HasBuiltins m => String -> m (Maybe Term) Source #

getName' :: HasBuiltins m => String -> m (Maybe QName) Source #

getTerm :: HasBuiltins m => String -> String -> m Term Source #

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

constructorForm :: Term -> TCM Term Source #

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term Source #

getBuiltinName' :: HasBuiltins m => String -> m (Maybe QName) Source #

getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName) Source #

isPrimitive :: HasBuiltins m => String -> QName -> m Bool Source #

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

idViewAsPath :: HasBuiltins m => Type -> m PathView Source #

Non dependent Path

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type Source #

Revert the EqualityView.

Postcondition: type is reduced.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.

getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName) Source #