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

chore(library): remove outdated comments

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-31 08:37:24 -07:00
parent 01af780b6e
commit a53ac25ca8
2 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/algebra/field.lean
View file

@ -454,10 +454,3 @@ section discrete_field
end discrete_field
end algebra
/-
decidable.by_cases
(assume Ha : a = 0, sorry)
(assume Ha : a ≠ 0, sorry)
-/

2
library/data/real/order.lean
View file

@ -6,8 +6,6 @@ The real numbers, constructed as equivalence classes of Cauchy sequences of rati
This construction follows Bishop and Bridges (1985).
To do:
o Break positive naturals into their own file and fill in sorry's
o Fill in sorrys for helper lemmas that will not be handled by simplifier
o Rename things and possibly make theorems private
-/