Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-13 00:32 4f32a4bc

View on Github →

feat(data/num/basic): to_nat' function for efficient nat -> num in VM

Estimated changes

Modified data/num/basic.lean

added def num.of_nat'

added def znum.of_int'

Modified data/num/lemmas.lean

added theorem num.cast_zero'

added theorem num.of_nat'_eq

added theorem num.of_nat_cast

added theorem pos_num.cast_one'

added theorem znum.cast_zero'

added theorem znum.of_int'_eq

added theorem znum.of_int_cast

added theorem znum.of_nat_cast