max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(init/meta/has_reflect): reflect 1

Browse source
This commit is contained in:
Sebastian Ullrich 2017-06-07 17:38:30 +02:00 • committed by Leonardo de Moura
parent 79f29a693e
commit 38aa99e7a5
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/meta/has_reflect.lean
View file

@ -17,6 +17,7 @@ local attribute [semireducible] reflected
meta instance nat.reflect : has_reflect ℕ
| n := if n = 0 then `(nat.zero)
else if n = 1 then `(1 : nat)
else if n % 2 = 0 then `(bit0 %%(nat.reflect (n / 2)) : ℕ)
else `(bit1 %%(nat.reflect (n / 2)) : ℕ)