Mathlib v3 is deprecated. Go to Mathlib v4

Def cast_num

Modification history

2020-10-15 08:51

src/data/num/basic.lean

lint(data/num/*): add docs and remove some [has_zero] requirements (#4604)

Modified cast_num View on Github →

2017-07-23 15:16

data/num/basic.lean

refactor(*): import content from lean/library/data and library_dev

Added cast_num View on Github →