Documentation

Lean.Meta.Tactic.Grind.AC.Eq

source
@[specialize #[]]
def Lean.Meta.Grind.AC.withExprs (a b : Expr) (k : ACM Unit) :
GoalM Unit

For each structure s s.t. a and b are elements of, execute k

Instances For
    source
    def Lean.Meta.Grind.AC.asACExpr (e : Expr) :
    ACM Grind.AC.Expr
    Instances For
      source
      def Lean.Meta.Grind.AC.norm (e : Grind.AC.Expr) :
      ACM Grind.AC.Seq
      Instances For
        source
        def Lean.Meta.Grind.AC.processNewEq (a b : Expr) :
        GoalM Unit
        Instances For
          source
          def Lean.Meta.Grind.AC.processNewDiseq (a b : Expr) :
          GoalM Unit
          Instances For
            source
            def Lean.Meta.Grind.AC.EqCnstr.simplifyRHS (c : EqCnstr) :
            ACM EqCnstr

            Simplifies the right-hand-side of the given equation.

            Instances For
              source
              structure Lean.Meta.Grind.AC.EqData :
              Type

              Data for equality propagation. We maintain a mapping from sequences to EqData

              Instances For
                source
                def Lean.Meta.Grind.AC.mkEqData (e : Expr) (r : Grind.AC.Expr) :
                ACM EqData
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Lean.Meta.Grind.AC.PropagateEqMap :
                  Type
                  Instances For
                    source
                    def Lean.Meta.Grind.AC.check :
                    GoalM CheckResult
                    Instances For
                      source
                      def Lean.Meta.Grind.AC.check' :
                      GoalM Bool
                      Instances For