- 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
- = 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
- data OutputForm' a b = OfType' {}
- 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
- 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
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 |
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 Source
A subset of OutputForm
.
(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 -> bSource
judgToOutputForm :: Judgement a c -> OutputForm a cSource
getConstraint :: Int -> TCM (OutputForm Expr Expr)Source
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)Source
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)Source
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputForm' Expr Name]Source
typeInCurrent :: Rewrite -> Expr -> TCM ExprSource
Returns the type of the expression in the current environment
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.