| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Expr | Source

giveExpr :: MetaId -> Expr -> TCM Expr | Source

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 Expr | Source

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> Expr -> TCM Expr | Source

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 |

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 | Source

A subset of `OutputForm`.
Constructors

OfType' |

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 | Source

showComparison :: Comparison -> String | Source

judgToOutputForm :: Judgement a c -> OutputForm a c | Source

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 Expr | Source

Returns the type of the expression in the current environment

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

withInteractionId :: InteractionId -> TCM a -> TCM a | Source

withMetaId :: MetaId -> TCM a -> TCM a | Source

introTactic :: InteractionId -> TCM [String] | Source

Produced by Haddock version 2.4.2