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

fix(library/data/real/order): mark '2' as local notation

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-31 15:03:18 -10:00
parent 86b10ab184
commit ea05ce7fe9
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/order.lean
View file

@ -15,7 +15,7 @@ open -[coercions] nat
open eq eq.ops pnat open eq eq.ops pnat
local notation 0 := rat.of_num 0 local notation 0 := rat.of_num 0
local notation 1 := rat.of_num 1 local notation 1 := rat.of_num 1
notation 2 := subtype.tag (of_num 2) dec_trivial local notation 2 := subtype.tag (of_num 2) dec_trivial
---------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------