Documentation

Interval.Tactic.Init

Interval tactics setup #

Aesop rule set for approx #

This module defines the Approx Aesop rule set which is used by the approx tactic. Aesop rule sets only become visible once the file in which they're declared is imported, so we must put this declaration into its own file.

Trace classes for the interval tactic #

Simp lemma sets #

source
def Parser.Attr.to_if :
Lean.ParserDescr

Simp lemmas for cleaning up bif statements

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Parser.Attr.to_if_proc :
    Lean.ParserDescr

    Simplification procedure

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Parser.Attr.to_bitvec_proc :
      Lean.ParserDescr

      Simplification procedure

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Parser.Attr.to_bitvec :
        Lean.ParserDescr

        Simp lemmas for reducing from Int64 and UInt64 to BitVec

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Parser.Attr.to_omega_proc :
          Lean.ParserDescr

          Simplification procedure

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Parser.Attr.to_omega :
            Lean.ParserDescr

            Simp lemmas for reducing from Int64 and UInt64 to ℕ and ℤ as prep for omega

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For