Documentation

Aesop.Script.StructureDynamic

  • The tactic invocation steps corresponding to the original unstructured script, but with MVarId keys adjusted to fit the current MetaM state. This state evolves during dynamic structuring and we continually update the steps so that this map's keys refer to metavariables which exist in the current MetaM state.

Instances For
    Instances For

      Given a bijective map map from new MVarIds to old MVarIds, update the steps of the context c such that each entry whose key is an old MVarId m is replaced with an entry whose key is the corresponding new MVarId map⁻¹ m.

      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              Equations
                Instances For
                  def Aesop.Script.withUpdatedMVarIds {α : Type} (oldPostState newPostState : Lean.Meta.SavedState) (oldPostGoals newPostGoals : Array Lean.MVarId) (onFailure onSuccess : DynStructureM α) :
                  Equations
                    Instances For
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For