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

chore: remove workarounds

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-19 09:44:57 -07:00
parent 544421faf5
commit 9fed5bda7d
2 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Data/Nat/Div.lean
View file

@ -18,8 +18,7 @@ protected def div (x y : @& Nat) : Nat :=
Nat.div (x - y) y + 1
else
0
decreasing_by
decreasing_with apply div_rec_lemma; assumption
decreasing_by apply div_rec_lemma; assumption
instance : Div Nat := ⟨Nat.div⟩
@ -37,8 +36,7 @@ theorem div.inductionOn.{u}
ind x y h (inductionOn (x - y) y ind base)
else
base x y h
decreasing_by
decreasing_with apply div_rec_lemma; assumption
decreasing_by apply div_rec_lemma; assumption
@[extern "lean_nat_mod"]
protected def mod (x y : @& Nat) : Nat :=
@ -46,8 +44,7 @@ protected def mod (x y : @& Nat) : Nat :=
Nat.mod (x - y) y
else
x
decreasing_by
decreasing_with apply div_rec_lemma; assumption
decreasing_by apply div_rec_lemma; assumption
instance : Mod Nat := ⟨Nat.mod⟩

1
src/Init/Data/Nat/Log2.lean
View file

@ -25,5 +25,4 @@ Computes `⌊max 0 (log₂ n)⌋`.
@[extern "lean_nat_log2"]
def log2 (n : @& Nat) : Nat :=
if h : n ≥ 2 then log2 (n / 2) + 1 else 0
termination_by _ n => n
decreasing_by exact log2_terminates _ h