michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library): remove unnecessary [fact] modifier

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-02 16:06:55 -07:00
parent fc0f12101c
commit 6077b3158c
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/int/basic.lean
View file

@ -591,7 +591,7 @@ subst (add_comm b c) (subst (add_comm a c) (sub_add_add_right a b c))
-- TODO: fix this
theorem dist_def (n m : ℕ) : dist n m = (to_nat (of_nat n - m)) :=
have H [fact] : of_nat n - m = psub (pair n m), from
have H : of_nat n - m = psub (pair n m), from
calc
psub (pair n 0) + -psub (pair m 0) = psub (pair (n + 0) (0 + m)) : by simp
... = psub (pair n m) : by simp,

4
library/data/nat/div.lean
View file

@ -73,7 +73,7 @@ let f := rec_measure default measure rec_val in
case_strong_induction_on m
(take x,
have H1 : f' 0 x = default, from rfl,
have H2 [fact]: ¬ measure x < 0, from not_lt_zero,
have H2 : ¬ measure x < 0, from not_lt_zero,
have H3 : restrict default measure f 0 x = default, from if_neg H2,
show f' 0 x = restrict default measure f 0 x, from trans H1 (symm H3))
(take m,
@ -88,7 +88,7 @@ case_strong_induction_on m
calc
f' m z = restrict default measure f m z : IH m le_refl z
... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)),
have H2 [fact] : f' (succ m) x = rec_val x f, from
have H2 : f' (succ m) x = rec_val x f, from
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = rec_val x (f' m) : if_pos H1