Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq

source
def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.applyEq? (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DiseqCnstr) :
LinearM (Option DiseqCnstr)

Given an equation c₁ containing the monomial a*x, and a disequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Grind.Arith.Linear.inSameStruct? (a b : Expr) :
    GoalM (Option Nat)

    Returns some structId if a and b are elements of the same structure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Grind.Arith.Linear.EqCnstr.norm (c : EqCnstr) :
      LinearM (Nat × Var × EqCnstr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.applySubsts (c : EqCnstr) :
        LinearM EqCnstr
        source
        def Lean.Meta.Grind.Arith.Linear.IneqCnstr.applyEq (a : Nat) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : IneqCnstr) :
        LinearM IneqCnstr

        Given an equation c₁ containing the monomial a*x, and an inequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.ignore (c : DiseqCnstr) :
          LinearM Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.applySubsts? (c₂ : DiseqCnstr) :
            LinearM (Option DiseqCnstr)
            source
            def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.assert (c : DiseqCnstr) :
            LinearM Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lean.Meta.Grind.Arith.Linear.EqCnstr.assert (c : EqCnstr) :
              LinearM Unit
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[export lean_process_linarith_eq]
                def Lean.Meta.Grind.Arith.Linear.processNewEqImpl (a b : Expr) :
                GoalM Unit
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[export lean_process_linarith_diseq]
                  def Lean.Meta.Grind.Arith.Linear.processNewDiseqImpl (a b : Expr) :
                  GoalM Unit
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For