# Rule Tactic Types #

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.`patternInstantiations`

: if the rule has a pattern, the pattern instantiations that were found in the goal. Each instantiation is a list of expressions which were found by matching the pattern against expressions in the goal. For example, if`h : max a b = max a c`

appears in the goal and the rule has pattern`max x y`

, there will be two pattern instantiations`[a, b]`

(representing the substitution`{x ↦ a, y ↦ b}`

) and`[a, c]`

. If the rule does not have a pattern,`patternInstantiations`

is empty; otherwise it's guaranteed to be non-empty.`options`

: the options given to Aesop.

- goal : Lean.MVarId
- mvars : Aesop.UnorderedArraySet Lean.MVarId
- indexMatchLocations : Std.HashSet Aesop.IndexMatchLocation
- patternInstantiations : Std.HashSet Aesop.RulePatternInstantiation
- options : Aesop.Options'

## Instances For

## Equations

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

A subgoal produced by a rule.

- mvarId : Lean.MVarId
The goal mvar.

- diff : Aesop.GoalDiff
A diff between the goal the rule was run on and this goal. Many

`MetaM`

tactics report information that allows you to easily construct a`GoalDiff`

. If you don't have access to such information, use`diffGoals`

, but note that it may not give optimal results.

## Instances For

## Equations

- Aesop.instInhabitedSubgoal = { default := { mvarId := default, diff := default } }

## Equations

- Aesop.mvarIdToSubgoal parentMVarId mvarId fvarSubst = do let __do_lift ← Aesop.diffGoals parentMVarId mvarId fvarSubst pure { mvarId := mvarId, diff := __do_lift }

## Instances For

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.`scriptSteps?`

: script steps which produce the same effect as the rule tactic. If`input.options.generateScript = false`

(where`input`

is the`RuleTacInput`

), this field is ignored. If the tactic does not support script generation, use`none`

.`successProbability`

: The success probability of this rule application. If`none`

, we use the success probability of the applied rule.

- goals : Array Aesop.Subgoal
- postState : Lean.Meta.SavedState
- scriptSteps? : Option (Array Aesop.Script.LazyStep)
- successProbability? : Option Aesop.Percent

## Instances For

## Equations

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

## Instances For

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

- applications : Array Aesop.RuleApplication

## Instances For

## Equations

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

## Equations

- Aesop.instInhabitedRuleTac = id inferInstance

## Equations

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

## Instances For

## Instances For

## Equations

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

## Instances For

A tactic generator is a special sort of rule tactic, intended for use with
generative machine learning methods. It generates zero or more tactics
(represented as strings) that could be applied to the goal, plus a success
probability for each tactic. When Aesop executes a tactic generator, it executes
each of the tactics and, if the tactic succeeds, adds a rule application for it.
The tactic's success probability (which must be between 0 and 1, inclusive)
becomes the success probability of the rule application. A `TacGen`

rule
succeeds if at least one of its suggested tactics succeeds.

## Equations

- Aesop.TacGen = (Lean.MVarId → Lean.MetaM (Array (String × Float)))

## Instances For

# Rule Tactic Descriptions #

## Instances For

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

## Instances For

## Equations

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

- const: Lean.Name → Aesop.RuleTerm
- term: Lean.Term → Aesop.RuleTerm

## Instances For

- apply: Aesop.RuleTerm → Lean.Meta.TransparencyMode → Option Aesop.RulePattern → Aesop.RuleTacDescr
- constructors: Array Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
- forward: Aesop.RuleTerm → Option Aesop.RulePattern → Aesop.UnorderedArraySet Nat → Bool → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
- cases: Aesop.CasesTarget → Lean.Meta.TransparencyMode → Bool → Array Aesop.CtorNames → Aesop.RuleTacDescr
- tacticM: Lean.Name → Aesop.RuleTacDescr
- ruleTac: Lean.Name → Aesop.RuleTacDescr
- tacGen: Lean.Name → Aesop.RuleTacDescr
- singleRuleTac: Lean.Name → Aesop.RuleTacDescr
- tacticStx: Lean.Syntax → Aesop.RuleTacDescr
- preprocess: Aesop.RuleTacDescr

## Instances For

## Equations

- Aesop.instInhabitedRuleTacDescr = { default := Aesop.RuleTacDescr.constructors default default }