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

Agda.Interaction.BasicOps

Synopsis

Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

evalInCurrent :: Expr -> TCM Expr

Evaluate the given expression in the current environment

data OutputForm' a b

A subset of OutputForm.

Constructors

OfType' 

Fields

ofName :: b
 
ofExpr :: a
 

Instances

typeInCurrent :: Rewrite -> Expr -> TCM Expr

Returns the type of the expression in the current environment

withMetaId :: MetaId -> TCM a -> TCM a

atTopLevel :: TCM a -> TCM a

Runs the given computation as if in an anonymous goal at the end of the top-level module.

moduleContents

Arguments

:: Range

The range of the next argument.

-> String

The module name.

-> TCM ([Name], [(Name, Type)])

Module names, names paired up with corresponding types.

Returns the contents of the given module.