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

Safe HaskellNone

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 Rewrite

Instances

rewrite :: (Normalise a, Reduce a) => Rewrite -> a -> TCMT IO a

data OutputConstraint' a b

A subset of OutputConstraint.

Constructors

OfType' 

Fields

ofName :: b
 
ofExpr :: a
 

typeInCurrent :: Rewrite -> Expr -> TCM Expr

Returns the type of the expression in the current environment We wake up irrelevant variables just in case the user want to invoke that command in an irrelevant context.

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.