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

data OutputForm' a b Source

A subset of OutputForm. Constructors OfType' ofName :: b ofExpr :: a

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.6.0