mathlib3
306801e1 - chore(data/nat/basic): split out even_odd_rec (#17759)

Commit
3 years ago
chore(data/nat/basic): split out even_odd_rec (#17759) `even_odd_rec` is annoying to port, because it is thoroughly tangled with `bit0` and `bit1`. It isn't used in mathlib, so I'm dumping it into its own file so we can get on with porting the critical `data.nat.basic` without delaying for this. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading