mathlib
151bcbe2 - feat(meta/expr,data/rat/basic): add rat.reflect (#1565)

Commit
6 years ago
feat(meta/expr,data/rat/basic): add rat.reflect (#1565) * feat(meta/expr,data/rat/basic): add rat.reflect * doc(meta/expr,data/rat/basic): clarify type restrictions for mk_numeral functions * fix name clash with norm_num functions * fix doc string to expr.of_rat * Update src/data/rat/basic.lean Co-Authored-By: Reid Barton <rwbarton@gmail.com> * fix declaration and move to new file * tests * fix import * protect rat.reflect * to_pos_rat --> to_nonneg_rat * correctly test rat.reflect
Author
Committer
Parents
Loading