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