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
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.
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.
MetaMstate after the tactic was run.
scriptBuilder?: script builder for the tactic. If
input.options.generateScript = false(where
RuleTacInput), this field is ignored, so you can use
none. If the tactic does not support script generation, also use
successProbability: The success probability of this rule application. If
none, we use the success probability of the applied rule.
- postState : Lean.Meta.SavedState
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
succeeds if at least one of its suggested tactics succeeds.
Rule Tactic Descriptions #
- 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
- tacGen: Lean.Name → Aesop.RuleTacDescr
- singleRuleTac: Lean.Name → Aesop.RuleTacDescr
- preprocess: Aesop.RuleTacDescr