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

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

Parses an expression.

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

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

atTopLevel :: TCM a -> TCM a Source

Runs the given computation as if in an anonymous goal at the end of the top-level module.

moduleContents Source

:: Range The range of the next argument. -> String The 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