Documentation

Lean.Meta.Tactic.Grind.AC.Util

source
def Lean.Meta.Grind.AC.get' :
GoalM State
Instances For
    source
    @[inline]
    def Lean.Meta.Grind.AC.modify' (f : State → State) :
    GoalM Unit
    Instances For
      source
      def Lean.Meta.Grind.AC.checkMaxSteps :
      GoalM Bool
      Instances For
        source
        def Lean.Meta.Grind.AC.incSteps :
        GoalM Unit
        Instances For
          source
          structure Lean.Meta.Grind.AC.ACM.Context :
          Type
          Instances For
            source
            class Lean.Meta.Grind.AC.MonadGetStruct (m : Type → Type) :
            Type
            Instances
              source
              @[implicit_reducible, always_inline]
              instance Lean.Meta.Grind.AC.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] :
              MonadGetStruct n
              source
              @[reducible, inline]
              abbrev Lean.Meta.Grind.AC.ACM (α : Type) :
              Type
              Instances For
                source
                @[reducible, inline]
                abbrev Lean.Meta.Grind.AC.ACM.run {α : Type} (opId : Nat) (x : ACM α) :
                GoalM α
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Lean.Meta.Grind.AC.getOpId :
                  ACM Nat
                  Instances For
                    source
                    def Lean.Meta.Grind.AC.ACM.getStruct :
                    ACM Struct
                    Instances For
                      source
                      @[implicit_reducible]
                      instance Lean.Meta.Grind.AC.instMonadGetStructACM :
                      MonadGetStruct ACM
                      source
                      def Lean.Meta.Grind.AC.modifyStruct (f : Struct → Struct) :
                      ACM Unit
                      Instances For
                        source
                        def Lean.Meta.Grind.AC.getOp :
                        ACM Expr
                        Instances For
                          source
                          def Lean.Meta.Grind.AC.getTermOpIds (e : Expr) :
                          GoalM (List Nat)
                          Instances For
                            source
                            def Lean.Meta.Grind.AC.addTermOpId (e : Expr) :
                            ACM Unit
                            Instances For
                              source
                              def Lean.Meta.Grind.AC.mkVar (e : Expr) :
                              ACM Grind.AC.Var
                              Instances For
                                source
                                def Lean.Meta.Grind.AC.getOpId? (op : Expr) :
                                GoalM (Option Nat)
                                Instances For
                                  source
                                  def Lean.Meta.Grind.AC.isOp? (e : Expr) :
                                  ACM (Option (Expr × Expr))
                                  Instances For
                                    source
                                    def Lean.Meta.Grind.AC.isCommutative :
                                    ACM Bool
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.AC.hasNeutral :
                                      ACM Bool
                                      Instances For
                                        source
                                        def Lean.Meta.Grind.AC.isIdempotent :
                                        ACM Bool
                                        Instances For