Commit 2021-02-13 00:49 30c2c5bf
View on Github →feat(data/fin): cast_succ_mk and other lemmas (#6094)
- add lemmas for all the
fin.cast_*
functions which describe what happens to an "explicitly presented" term offin n
, built from the constructor - fixes some errors in doc-strings