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

Agda.TypeChecking.Monad.Builtin

Synopsis

Documentation

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

Instances

Instances details
HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Names

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

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

Defined in Agda.TypeChecking.Monad.Builtin

(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

data CoinductionKit Source #

The coinductive primitives.

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 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

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.