Documentation

Lean.Meta.Tactic.LinearArith.Solver

Instances For
    @[reducible, inline]
    Equations
    • a.size = a.val.size
    Instances For
      @[reducible, inline]
      Equations
      • a.get? x = if h : x.id < a.size then some (a.val.get x.id, h) else none
      Instances For
        @[reducible, inline]
        Equations
        • a.push v = { val := a.val.push v }
        Instances For
          @[reducible, inline]
          Equations
          • a.shrink newSize = { val := a.val.shrink newSize }
          Instances For
            @[reducible, inline]
            Equations
            • e.size = e.val.size
            Instances For
              @[reducible, inline]
              Equations
              • e.getMaxVarCoeff = e.val.back.fst
              Instances For
                @[reducible, inline]
                Equations
                • e.getMaxVar = e.val.back.snd
                Instances For
                  @[reducible, inline]
                  Equations
                  • e.get i = e.val.get i
                  Instances For
                    Equations
                    Instances For
                      @[irreducible]
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        Instances For
                          @[irreducible]
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Instances For
                                Equations
                                @[reducible, inline]
                                Equations
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Instances For
                                          Equations
                                          @[reducible, inline]
                                          Equations
                                          • s.getNumVars = s.lowers.size
                                          Instances For
                                            @[reducible, inline]
                                            Equations
                                            • s.currVar = s.assignment.size
                                            Instances For
                                              @[reducible, inline]
                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  Equations
                                                  • s.assignCurr v = { lowers := s.lowers, uppers := s.uppers, int := s.int, assignment := s.assignment.push v }
                                                  Instances For
                                                    def Lean.Meta.Linear.pickAssignment? (lower : Lean.Rat) (lowerIsStrict : Bool) (upper : Lean.Rat) (upperIsStrict : Bool) :
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        Instances For