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

refactor(library/data/real/basic): declare 'real' in the toplevel like 'nat', 'int' and 'rat'

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-24 11:59:46 -07:00
parent 5c7a20e5bd
commit 99a9dec93f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1042,9 +1042,9 @@ end s
----------------------------------------------
-- take quotients to get ℝ and show it's a comm ring
namespace real
open s
definition real := quot reg_seq.to_setoid
namespace real
notation `ℝ` := real
definition add (x y : ℝ) : ℝ :=