- parseExpr :: Range -> String -> TCM Expr
- 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
- evalInMeta :: InteractionId -> Expr -> TCM Expr
- data Rewrite
- = AsIs
- | Instantiated
- | HeadNormal
- | Normalised
- data OutputForm a b = OutputForm ProblemId (OutputConstraint a b)
- data OutputConstraint a b
- = OfType b a
- | CmpInType Comparison a b b
- | CmpElim [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 (OutputConstraint a b) ProblemId
- | Assign b a
- | TypedAssign b a a
- | IsEmptyType a
- | FindInScopeOF b
- data OutputConstraint' a b = OfType' {}
- outputFormId :: OutputForm a b -> b
- showComparison :: Comparison -> String
- judgToOutputForm :: Judgement a c -> OutputConstraint a c
- getConstraints :: TCM [OutputForm Expr Expr]
- getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]
- typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr MetaId)
- typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
- typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
- typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr MetaId]
- contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name]
- typeInCurrent :: Rewrite -> Expr -> TCM Expr
- 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
- moduleContents :: Range -> String -> TCM ([Name], [(Name, Type)])
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM ExprSource
give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])Source
addDecl :: Declaration -> TCM [InteractionId]Source
refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr, [InteractionId])Source
evalInCurrent :: Expr -> TCM ExprSource
Evaluate the given expression in the current environment
evalInMeta :: InteractionId -> Expr -> TCM ExprSource
data OutputForm a b Source
Reify ProblemConstraint (Closure (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 OutputConstraint a b Source
OfType b a | |
CmpInType Comparison a b b | |
CmpElim [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 (OutputConstraint a b) ProblemId | |
Assign b a | |
TypedAssign b a a | |
IsEmptyType a | |
FindInScopeOF b |
Reify Constraint (OutputConstraint Expr Expr) | |
Functor (OutputConstraint a) | |
(Show a, Show b) => Show (OutputConstraint a b) | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) |
data OutputConstraint' a b Source
A subset of OutputConstraint
.
(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) |
outputFormId :: OutputForm a b -> bSource
judgToOutputForm :: Judgement a c -> OutputConstraint a cSource
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr MetaId)Source
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name]Source
typeInCurrent :: Rewrite -> Expr -> TCM ExprSource
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.
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM ExprSource
withInteractionId :: InteractionId -> TCM a -> TCM aSource
withMetaId :: MetaId -> TCM a -> TCM aSource
introTactic :: InteractionId -> TCM [String]Source
atTopLevel :: TCM a -> TCM aSource
Runs the given computation as if in an anonymous goal at the end of the top-level module.