- root : MVarClusterRef
- rootMetaState : Lean.Meta.SavedState
- numGoals : Nat
- numRapps : Nat
- nextGoalId : GoalId
- nextRappId : RappId
- allIntroducedMVars : Std.HashSet Lean.MVarId
Union of the mvars introduced by all rapps.
Instances For
Equations
Instances For
- currentIteration : Iteration
- ruleSet : LocalRuleSet