Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.BasicOps
Synopsis
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' {
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)
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
parseExpr :: Range -> String -> TCM ExprSource
Parses an expression.
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
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 Source
A subset of OutputForm.
Constructors
OfType'
ofName :: b
ofExpr :: a
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
typesOfVisibleMetas :: Rewrite -> TCM [OutputForm Expr InteractionId]Source
typesOfHiddenMetas :: Rewrite -> TCM [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
atTopLevel :: TCM a -> TCM aSource
Runs the given computation as if in an anonymous goal at the end of the top-level module.
moduleContentsSource
:: RangeThe range of the next argument.
-> StringThe module name.
-> TCM ([Name], [(Name, Type)])Module names, names paired up with corresponding types.
Returns the contents of the given module.
Produced by Haddock version 2.6.1