Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.BasicOps
Synopsis
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
| JustType b
| CmpTypes 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' {
ofName :: b
ofExpr :: a
}
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)
typeOfMetas :: Rewrite -> TCM ([OutputForm Expr InteractionId], [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]
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM ExprSource
giveExpr :: MetaId -> Expr -> 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 Rewrite Source
Constructors
AsIs
Instantiated
HeadNormal
Normalised
data OutputForm a b Source
Constructors
OfType b a
CmpInType Comparison a b b
JustType b
CmpTypes 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
show/hide Instances
data OutputForm' a b Source
A subset of OutputForm.
Constructors
OfType'
ofName :: b
ofExpr :: a
show/hide Instances
outputFormId :: OutputForm a b -> bSource
showComparison :: Comparison -> StringSource
judgToOutputForm :: Judgement a c -> OutputForm a cSource
getConstraint :: Int -> TCM (OutputForm Expr Expr)Source
getConstraints :: TCM [OutputForm Expr Expr]Source
getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]Source
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)Source
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)Source
typeOfMetas :: Rewrite -> TCM ([OutputForm Expr InteractionId], [OutputForm Expr MetaId])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
Produced by Haddock version 2.4.2