Simproc for intervals of natural numbers

@[irreducible]

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 ℤ.

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).

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.

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.

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.

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.

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.

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.

ℕ

ℤ