Rule Tactic Types

structure Aesop.RuleTacInput : Type

• goal : Lean.MVarId
• mvars : Aesop.UnorderedArraySet Lean.MVarId
• indexMatchLocations : Aesop.UnorderedArraySet Aesop.IndexMatchLocation
• options : Aesop.Options'

Input for a rule tactic. Contains:

• goal: the goal on which the rule is run.
• mvars: the set of mvars which occur in goal.
• indexMatchLocations: if the rule is indexed, the locations (e.g. hyps or the target) matched by the rule's index entries. Otherwise an empty set.

instance Aesop.instInhabitedRuleTacInput : Inhabited Aesop.RuleTacInput

Equations

• Aesop.instInhabitedRuleTacInput = { default := { goal := default, mvars := default, indexMatchLocations := default, options := default } }

structure Aesop.RuleApplication : Type

• goals : Array Lean.MVarId
• postState : Lean.Meta.SavedState
• scriptBuilder? : Option Aesop.RuleTacScriptBuilder

A single rule application, representing the application of a tactic to the input goal. Must accurately report the following information:

• goals: the goals generated by the tactic.
• postState: the MetaM state after the tactic was run.
• scriptBuilder?: script builder for the tactic. If input.options.generateScript = false (where input is the RuleTacInput), this field is ignored, so you can use none. If the tactic does not support script generation, also use none.

def Aesop.RuleApplication.check (r : Aesop.RuleApplication) : Lean.MetaM (Option Lean.MessageData)

Equations

• One or more equations did not get rendered due to their size.

structure Aesop.RuleTacOutput : Type

• applications : Array Aesop.RuleApplication

The result of a rule tactic is a list of rule applications.

instance Aesop.instInhabitedRuleTacOutput : Inhabited Aesop.RuleTacOutput

Equations

• Aesop.instInhabitedRuleTacOutput = { default := { applications := default } }

def Aesop.RuleTac : Type

A RuleTac is the tactic that is run when a rule is applied to a goal.

Equations

• Aesop.RuleTac = (Aesop.RuleTacInput → Lean.MetaM Aesop.RuleTacOutput)

instance Aesop.instInhabitedRuleTac : Inhabited Aesop.RuleTac

Equations

• Aesop.instInhabitedRuleTac = id inferInstance

def Aesop.SingleRuleTac : Type

A RuleTac which generates only a single RuleApplication.

Equations

• Aesop.SingleRuleTac = (Aesop.RuleTacInput → Lean.MetaM (Array Lean.MVarId × Option Aesop.RuleTacScriptBuilder))

@[inline]

def Aesop.SingleRuleTac.toRuleTac (t : Aesop.SingleRuleTac) : Aesop.RuleTac

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Aesop.RuleTac.ofSingleRuleTac (t : Aesop.SingleRuleTac) : Aesop.RuleTac

Equations

• Aesop.RuleTac.ofSingleRuleTac = Aesop.SingleRuleTac.toRuleTac

Rule Tactic Descriptions

def Aesop.CasesPattern : Type

Equations

• Aesop.CasesPattern = Lean.Meta.AbstractMVarsResult

inductive Aesop.CasesTarget : Type

• decl: Lean.Name → Aesop.CasesTarget
• patterns: Array Aesop.CasesPattern → Aesop.CasesTarget

instance Aesop.instInhabitedCasesTarget : Inhabited Aesop.CasesTarget

Equations

• Aesop.instInhabitedCasesTarget = { default := Aesop.CasesTarget.decl default }

inductive Aesop.RuleTacDescr : Type

• applyConst: Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• applyFVar: Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• constructors: Array Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• forwardConst: Lean.Name → Aesop.UnorderedArraySet Nat → Bool → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• forwardFVar: Lean.Name → Aesop.UnorderedArraySet Nat → Bool → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• cases: Aesop.CasesTarget → Lean.Meta.TransparencyMode → Bool → Aesop.RuleTacDescr
• tacticM: Lean.Name → Aesop.RuleTacDescr
• ruleTac: Lean.Name → Aesop.RuleTacDescr
• singleRuleTac: Lean.Name → Aesop.RuleTacDescr
• preprocess: Aesop.RuleTacDescr

instance Aesop.instInhabitedRuleTacDescr : Inhabited Aesop.RuleTacDescr

Equations

• Aesop.instInhabitedRuleTacDescr = { default := Aesop.RuleTacDescr.applyConst default default }

def Aesop.RuleTacDescr.isGlobal : Aesop.RuleTacDescr → Bool

Equations

• One or more equations did not get rendered due to their size.