Agda.Interaction.BasicOps

Documentation

parseExpr :: Range -> String -> TCM Expr

Parses an expression.

parseExprIn :: InteractionId -> Range -> String -> TCM Expr

giveExpr :: MetaId -> Expr -> TCM Expr

give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])

addDecl :: Declaration -> TCM [InteractionId]

refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])

evalInCurrent :: Expr -> TCM Expr

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> Expr -> TCM Expr

data Rewrite

Constructors

AsIs

Instantiated

HeadNormal

Normalised

data OutputForm a b

Constructors

OfType b a

CmpInType Comparison a b b

CmpTerms [Polarity] a [b] [b]

JustType b

CmpTypes Comparison b b

CmpLevels Comparison b b

CmpTeles Comparison b b

JustSort b

CmpSorts Comparison b b

Guard (OutputForm a b) [OutputForm a b]

Assign b a

TypedAssign b a a

IsEmptyType a

Instances

Reify Constraint (OutputForm Expr Expr)

Functor (OutputForm a)

(Show a, Show b) => Show (OutputForm a b)

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d)

data OutputForm' a b

A subset of OutputForm.

Constructors

OfType'

Fields

ofName :: b

ofExpr :: a

Instances

(Pretty a, Pretty b) => Pretty (OutputForm' a b)

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm' a b) (OutputForm' c d)

outputFormId :: OutputForm a b -> b

showComparison :: Comparison -> String

judgToOutputForm :: Judgement a c -> OutputForm a c

getConstraint :: Int -> TCM (OutputForm Expr Expr)

getConstraints :: TCM [OutputForm Expr Expr]

getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)

typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)

typesOfVisibleMetas :: Rewrite -> TCM [OutputForm Expr InteractionId]

typesOfHiddenMetas :: Rewrite -> TCM [OutputForm Expr MetaId]

contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputForm' Expr Name]

typeInCurrent :: Rewrite -> Expr -> TCM Expr

Returns the type of the expression in the current environment

typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr

withInteractionId :: InteractionId -> TCM a -> TCM a

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

introTactic :: InteractionId -> TCM [String]

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.