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

chore: fix Less name

Browse source
This commit is contained in:
Marc Huisinga 2020-11-21 12:07:19 +01:00 • committed by Sebastian Ullrich
parent 278cd1aefc
commit 5c07f20c3b
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/Json/Basic.lean
View file

@ -78,10 +78,10 @@ def lt (a b : JsonNumber) : Bool :=
else if ae > be then false
else am < bm
def ltProp : Less JsonNumber :=
def ltProp : HasLess JsonNumber :=
⟨fun a b => lt a b = true⟩
instance : Less JsonNumber :=
instance : HasLess JsonNumber :=
ltProp
instance (a b : JsonNumber) : Decidable (a < b) :=

4
src/Lean/Data/JsonRpc.lean
View file

@ -103,10 +103,10 @@ private def RequestID.lt : RequestID → RequestID → Bool
| RequestID.num _, RequestID.str _ => true
| _, _ /- str < *, num < null, null < null -/ => false
private def RequestID.ltProp : Less RequestID :=
private def RequestID.ltProp : HasLess RequestID :=
⟨fun a b => RequestID.lt a b = true⟩
instance : Less RequestID :=
instance : HasLess RequestID :=
RequestID.ltProp
instance (a b : RequestID) : Decidable (a < b) :=