Documentation

SSA.Experimental.Bits.AutoStructs.Tactic

source
def AutoStructs.Term.toExpr (t : AutoStructs.Term) :
Lean.Expr
Equations
Instances For
    source
    def AutoStructs.Relation.toExpr (rel : AutoStructs.Relation) :
    Lean.Expr
    Equations
    Instances For
      source
      def AutoStructs.Binop.toExpr (rel : AutoStructs.Binop) :
      Lean.Expr
      Equations
      Instances For
        source
        def AutoStructs.Unop.toExpr (rel : AutoStructs.Unop) :
        Lean.Expr
        Equations
        Instances For
          source
          def AutoStructs.Formula.toExpr (φ : AutoStructs.Formula) :
          Lean.Expr
          Equations
          Instances For
            source
            instance instToExprFormula :
            Lean.ToExpr AutoStructs.Formula
            Equations
            source
            structure Tactic.State :
            Type
            Instances For
              source
              instance Tactic.instInhabitedState :
              Inhabited Tactic.State
              Equations
              source
              @[reducible, inline]
              abbrev Tactic.M (α : Type) :
              Type
              Equations
              Instances For
                source
                def Tactic.addAsVar (e : Lean.Expr) :
                Tactic.M AutoStructs.Term
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Tactic.checkBVs (es : List Lean.Expr) :
                  Tactic.M Bool
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def Tactic.parseTerm (e : Lean.Expr) :
                    Tactic.M AutoStructs.Term
                    source
                    partial def Tactic.parseFormula (e : Lean.Expr) :
                    Tactic.M AutoStructs.Formula
                    source
                    axiom Tactic.automaton_axiom (A : Prop) :
                    A
                    source
                    def Tactic.mkFinLit (m : ℕ) (n : ℕ) :
                    Lean.MetaM Lean.Expr
                    Equations
                    Instances For
                      source
                      def Tactic.mkBitVecLit0 (w : Lean.Expr) :
                      Lean.MetaM Lean.Expr
                      Equations
                      Instances For
                        source
                        def Tactic.listExprExpr (es : List Lean.Expr) (type : Lean.Expr) :
                        Lean.Expr
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Tactic.arrayExprExpr (es : Array Lean.Expr) (type : Lean.Expr) :
                          Lean.Expr
                          Equations
                          Instances For
                            source
                            def Tactic.tacticBv_automata_inner :
                            Lean.ParserDescr
                            Equations
                            Instances For
                              source
                              def Tactic.tacticBv_automata' :
                              Lean.ParserDescr
                              Equations
                              Instances For
                                source
                                theorem dfadfa (w : ℕ) (x : BitVec w) :
                                (0 >ₛ x) = true ↔ x.msb = true
                                source
                                theorem and_ule_not_xor (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                (~~~(x ^^^ y) ≥ᵤ x &&& y) = true
                                source
                                theorem xor_ule_or (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                (x ||| y ≥ᵤ x ^^^ y) = true
                                source
                                theorem ult_iff_not_ule (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                (y >ᵤ x) = true ↔ ¬(x ≥ᵤ y) = true
                                source
                                theorem sub_neg_sub (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                x - y = -(y - x)
                                source
                                theorem eq_iff_not_sub_or_sub (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                x = y ↔ (~~~(x - y ||| y - x)).msb = true
                                source
                                theorem lt_iff_sub_xor_xor_and_sub_xor (w : ℕ) (x : BitVec w) (y : BitVec w) :
                                (y >ₛ x) = true ↔ (x - y ^^^ (x ^^^ y) &&& (x - y ^^^ x)).msb = true