Documentation

Aesop.Search.Expansion.Norm

Instances For
    Instances For
      @[reducible, inline]
      abbrev Aesop.NormM (α : Type) :
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Instances For
                    @[always_inline]
                    Equations
                      Instances For

                        On success, returns the rule tactic's result, the new forward state and the new forward rule matches. If rule corresponds to some forward rule matches, returns the matches as well.

                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        @[always_inline]
                                        def Aesop.checkSimp (name : String) (mayCloseGoal : Bool) (goal : Lean.MVarId) (x : NormM (Option NormRuleResult)) :
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        Equations
                                                          Instances For
                                                            def Aesop.runNormSteps (goal : Lean.MVarId) (steps : Array NormStep) (stepsNe : 0 < steps.size) :
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Instances For
                                                                        Equations
                                                                          Instances For