Documentation

Mathlib.Tactic.Simproc.FinsetInterval

Simproc for intervals of natural numbers #

source
partial def Mathlib.Tactic.Simp.evalFinsetIccNat (m n : ℕ) (em en : Q(ℕ)) :
Lean.MetaM ((s : Q(Finset ℕ)) × Q(Finset.Icc «$em» «$en» = «$s»))

Given natural numbers m and n and corresponding natural literals em and en, returns (s, ⊢ Finset.Icc m n = s).

This cannot be easily merged with evalFinsetIccInt since they require different handling of numerals for ℕ and ℤ.

source
partial def Mathlib.Tactic.Simp.evalFinsetIccInt (m n : ℤ) (em en : Q(ℤ)) :
Lean.MetaM ((s : Q(Finset ℤ)) × Q(Finset.Icc «$em» «$en» = «$s»))

Given integers m and n and corresponding integer literals em and en, returns (s, ⊢ Finset.Icc m n = s).

This cannot be easily merged with evalFinsetIccNat since they require different handling of numerals for ℕ and ℤ.

Note that these simprocs are not made simp to avoid simp blowing up on goals containing things of the form Iic (2 ^ 1024).

source
def Finset.Icc_ofNat_ofNat :
Lean.Meta.Simp.Simproc

Simproc to compute Finset.Icc a b where a and b are numerals.

Warnings:

  • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
  • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Finset.Ico_ofNat_ofNat :
    Lean.Meta.Simp.Simproc

    Simproc to compute Finset.Ico a b where a and b are numerals.

    Warnings:

    • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
    • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
    Instances For
      source
      def Finset.Ioc_ofNat_ofNat :
      Lean.Meta.Simp.Simproc

      Simproc to compute Finset.Ioc a b where a and b are numerals.

      Warnings:

      • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
      • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
      Instances For
        source
        def Finset.Ioo_ofNat_ofNat :
        Lean.Meta.Simp.Simproc

        Simproc to compute Finset.Ioo a b where a and b are numerals.

        Warnings:

        • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
        • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
        Instances For
          source
          def Finset.Iic_ofNat :
          Lean.Meta.Simp.Simproc

          Simproc to compute Finset.Iic b where b is a numeral.

          Warnings:

          • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
          • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Finset.Iio_ofNat :
            Lean.Meta.Simp.Simproc

            Simproc to compute Finset.Iio b where b is a numeral.

            Warnings:

            • With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
            • Make sure to exclude Finset.insert_eq_of_mem from your simp call when using this simproc. This avoids a quadratic time performance hit.
            Instances For

              ℕ #

              ℤ #