From dc6c1e329f3ba72c81da3732c33360c4e89bf0eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2019 02:52:01 -0700 Subject: [PATCH] refactor(library/init/data/rbmap): use Bool instead of Prop --- library/init/data/char/basic.lean | 10 ++- library/init/data/rbmap/basic.lean | 124 +++++++++++++--------------- library/init/data/rbtree/basic.lean | 14 ++-- library/init/lean/elaborator.lean | 14 ++-- library/init/lean/expander.lean | 6 +- library/init/lean/name.lean | 9 +- library/init/lean/parser/basic.lean | 3 +- library/init/lean/parser/trie.lean | 10 +-- library/init/lean/position.lean | 9 +- library/init/lean/trace.lean | 2 +- 10 files changed, 91 insertions(+), 110 deletions(-) diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index ae500ec5c4..8aa87ab9ce 100644 --- a/library/init/data/char/basic.lean +++ b/library/init/data/char/basic.lean @@ -30,11 +30,13 @@ else if v & 0xFE = 0xFC then 6 else if v = 0xFF then 1 else 0 -protected def lt (a b : Char) : Prop := a.val < b.val -protected def le (a b : Char) : Prop := a.val ≤ b.val +protected def Less (a b : Char) : Prop := a.val < b.val +protected def LessEq (a b : Char) : Prop := a.val ≤ b.val -instance : HasLess Char := ⟨Char.lt⟩ -instance : HasLessEq Char := ⟨Char.le⟩ +instance : HasLess Char := ⟨Char.Less⟩ +instance : HasLessEq Char := ⟨Char.LessEq⟩ + +protected def lt (a b : Char) : Bool := a.val < b.val instance decLt (a b : Char) : Decidable (a < b) := UInt32.decLt _ _ diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 2a72247ab9..628d9988c5 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.data.ordering.basic init.coe init.data.option.basic +import init.data.repr init.data.option.basic universes u v w w' @@ -13,7 +13,7 @@ inductive Rbcolor inductive RBNode (α : Type u) (β : α → Type v) | leaf {} : RBNode -| Node (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode +| node (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode namespace RBNode variables {α : Type u} {β : α → Type v} {σ : Type w} @@ -22,80 +22,79 @@ open Rbcolor Nat def depth (f : Nat → Nat → Nat) : RBNode α β → Nat | leaf := 0 -| (Node _ l _ _ r) := succ (f (depth l) (depth r)) +| (node _ l _ _ r) := succ (f (depth l) (depth r)) protected def min : RBNode α β → Option (Σ k : α, β k) | leaf := none -| (Node _ leaf k v _) := some ⟨k, v⟩ -| (Node _ l k v _) := min l +| (node _ leaf k v _) := some ⟨k, v⟩ +| (node _ l k v _) := min l protected def max : RBNode α β → Option (Σ k : α, β k) | leaf := none -| (Node _ _ k v leaf) := some ⟨k, v⟩ -| (Node _ _ k v r) := max r +| (node _ _ k v leaf) := some ⟨k, v⟩ +| (node _ _ k v r) := max r @[specialize] def fold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ | leaf b := b -| (Node _ l k v r) b := fold r (f k v (fold l b)) +| (node _ l k v r) b := fold r (f k v (fold l b)) @[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : RBNode α β → σ → m σ | leaf b := pure b -| (Node _ l k v r) b := do b₁ ← mfold l b, b₂ ← f k v b₁, mfold r b₂ +| (node _ l k v r) b := do b₁ ← mfold l b, b₂ ← f k v b₁, mfold r b₂ @[specialize] def revFold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ | leaf b := b -| (Node _ l k v r) b := revFold l (f k v (revFold r b)) +| (node _ l k v r) b := revFold l (f k v (revFold r b)) @[specialize] def all (p : Π k : α, β k → Bool) : RBNode α β → Bool | leaf := true -| (Node _ l k v r) := p k v && all l && all r +| (node _ l k v r) := p k v && all l && all r @[specialize] def any (p : Π k : α, β k → Bool) : RBNode α β → Bool | leaf := false -| (Node _ l k v r) := p k v || any l || any r +| (node _ l k v r) := p k v || any l || any r def singleton (k : α) (v : β k) : RBNode α β := -Node red leaf k v leaf +node red leaf k v leaf def balance1 : RBNode α β → RBNode α β → RBNode α β -| (Node _ _ kv vv t) (Node _ (Node red l kx vx r₁) ky vy r₂) := Node red (Node black l kx vx r₁) ky vy (Node black r₂ kv vv t) -| (Node _ _ kv vv t) (Node _ l₁ ky vy (Node red l₂ kx vx r)) := Node red (Node black l₁ ky vy l₂) kx vx (Node black r kv vv t) -| (Node _ _ kv vv t) (Node _ l ky vy r) := Node black (Node red l ky vy r) kv vv t +| (node _ _ kv vv t) (node _ (node red l kx vx r₁) ky vy r₂) := node red (node black l kx vx r₁) ky vy (node black r₂ kv vv t) +| (node _ _ kv vv t) (node _ l₁ ky vy (node red l₂ kx vx r)) := node red (node black l₁ ky vy l₂) kx vx (node black r kv vv t) +| (node _ _ kv vv t) (node _ l ky vy r) := node black (node red l ky vy r) kv vv t | _ _ := leaf -- unreachable def balance2 : RBNode α β → RBNode α β → RBNode α β -| (Node _ t kv vv _) (Node _ (Node red l kx₁ vx₁ r₁) ky vy r₂) := Node red (Node black t kv vv l) kx₁ vx₁ (Node black r₁ ky vy r₂) -| (Node _ t kv vv _) (Node _ l₁ ky vy (Node red l₂ kx₂ vx₂ r₂)) := Node red (Node black t kv vv l₁) ky vy (Node black l₂ kx₂ vx₂ r₂) -| (Node _ t kv vv _) (Node _ l ky vy r) := Node black t kv vv (Node red l ky vy r) +| (node _ t kv vv _) (node _ (node red l kx₁ vx₁ r₁) ky vy r₂) := node red (node black t kv vv l) kx₁ vx₁ (node black r₁ ky vy r₂) +| (node _ t kv vv _) (node _ l₁ ky vy (node red l₂ kx₂ vx₂ r₂)) := node red (node black t kv vv l₁) ky vy (node black l₂ kx₂ vx₂ r₂) +| (node _ t kv vv _) (node _ l ky vy r) := node black t kv vv (node red l ky vy r) | _ _ := leaf -- unreachable def isRed : RBNode α β → Bool -| (Node red _ _ _ _) := true +| (node red _ _ _ _) := true | _ := false section insert -variables (lt : α → α → Prop) [DecidableRel lt] +variables (lt : α → α → Bool) def ins : RBNode α β → Π k : α, β k → RBNode α β -| leaf kx vx := Node red leaf kx vx leaf -| (Node red a ky vy b) kx vx := - (match cmpUsing lt kx ky with - | Ordering.lt := Node red (ins a kx vx) ky vy b - | Ordering.Eq := Node red a kx vx b - | Ordering.gt := Node red a ky vy (ins b kx vx)) -| (Node black a ky vy b) kx vx := - match cmpUsing lt kx ky with - | Ordering.lt := - if isRed a then balance1 (Node black leaf ky vy b) (ins a kx vx) - else Node black (ins a kx vx) ky vy b - | Ordering.Eq := Node black a kx vx b - | Ordering.gt := - if isRed b then balance2 (Node black a ky vy leaf) (ins b kx vx) - else Node black a ky vy (ins b kx vx) +| leaf kx vx := node red leaf kx vx leaf +| (node red a ky vy b) kx vx := + if lt kx ky then node red (ins a kx vx) ky vy b + else if lt ky kx then node red a ky vy (ins b kx vx) + else node red a kx vx b +| (node black a ky vy b) kx vx := + if lt kx ky then + if isRed a then balance1 (node black leaf ky vy b) (ins a kx vx) + else node black (ins a kx vx) ky vy b + else if lt ky kx then + if isRed b then balance2 (node black a ky vy leaf) (ins b kx vx) + else node black a ky vy (ins b kx vx) + else + node black a kx vx b def setBlack : RBNode α β → RBNode α β -| (Node _ l k v r) := Node black l k v r +| (node _ l k v r) := node black l k v r | e := e def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β := @@ -105,39 +104,34 @@ else ins lt t k v end insert section membership -variable (lt : α → α → Prop) - -variable [DecidableRel lt] +variable (lt : α → α → Bool) def findCore : RBNode α β → Π k : α, Option (Σ k : α, β k) | leaf x := none -| (Node _ a ky vy b) x := - (match cmpUsing lt x ky with - | Ordering.lt := findCore a x - | Ordering.Eq := some ⟨ky, vy⟩ - | Ordering.gt := findCore b x) +| (node _ a ky vy b) x := + if lt x ky then findCore a x + else if lt ky x then findCore b x + else some ⟨ky, vy⟩ def find {β : Type v} : RBNode α (λ _, β) → α → Option β -| leaf x := none -| (Node _ a ky vy b) x := - (match cmpUsing lt x ky with - | Ordering.lt := find a x - | Ordering.Eq := some vy - | Ordering.gt := find b x) +| leaf x := none +| (node _ a ky vy b) x := + if lt x ky then find a x + else if lt ky x then find b x + else some vy def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β) | leaf x lb := lb -| (Node _ a ky vy b) x lb := - (match cmpUsing lt x ky with - | Ordering.lt := lowerBound a x lb - | Ordering.Eq := some ⟨ky, vy⟩ - | Ordering.gt := lowerBound b x (some ⟨ky, vy⟩)) +| (node _ a ky vy b) x lb := + if lt x ky then lowerBound a x lb + else if lt ky x then lowerBound b x (some ⟨ky, vy⟩) + else some ⟨ky, vy⟩ end membership -inductive WellFormed (lt : α → α → Prop) : RBNode α β → Prop +inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop | leafWff : WellFormed leaf -| insertWff {n n' : RBNode α β} {k : α} {v : β k} [DecidableRel lt] : WellFormed n → n' = insert lt n k v → WellFormed n' +| insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed n → n' = insert lt n k v → WellFormed n' end RBNode @@ -145,17 +139,17 @@ open RBNode /- TODO(Leo): define dRBMap -/ -def RBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) := +def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) := {t : RBNode α (λ _, β) // t.WellFormed lt } -@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : RBMap α β lt := +@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt := ⟨leaf, WellFormed.leafWff lt⟩ -instance (α : Type u) (β : Type v) (lt : α → α → Prop) : HasEmptyc (RBMap α β lt) := +instance (α : Type u) (β : Type v) (lt : α → α → Bool) : HasEmptyc (RBMap α β lt) := ⟨mkRBMap α β lt⟩ namespace RBMap -variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Prop} +variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool} def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat := t.val.depth f @@ -194,8 +188,6 @@ t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩ instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := ⟨λ t, "rbmapOf " ++ repr t.toList⟩ -variables [DecidableRel lt] - def insert : RBMap α β lt → α → β → RBMap α β lt | ⟨t, w⟩ k v := ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩ @@ -217,7 +209,7 @@ def lowerBound : RBMap α β lt → α → Option (Σ k : α, β) @[inline] def contains (t : RBMap α β lt) (a : α) : Bool := (t.find a).isSome -def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt := +def fromList (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt := l.foldl (λ r p, r.insert p.1 p.2) (mkRBMap α β lt) @[inline] def all : RBMap α β lt → (α → β → Bool) → Bool @@ -228,5 +220,5 @@ l.foldl (λ r p, r.insert p.1 p.2) (mkRBMap α β lt) end RBMap -def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt := +def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt := RBMap.fromList l lt diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index d3c9c2c897..8730cd219d 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -7,17 +7,17 @@ prelude import init.data.rbmap.basic universes u v w -def RBTree (α : Type u) (lt : α → α → Prop) : Type u := +def RBTree (α : Type u) (lt : α → α → Bool) : Type u := RBMap α Unit lt -@[inline] def mkRBTree (α : Type u) (lt : α → α → Prop) : RBTree α lt := +@[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt := mkRBMap α Unit lt -instance (α : Type u) (lt : α → α → Prop) : HasEmptyc (RBTree α lt) := +instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) := ⟨mkRBTree α lt⟩ namespace RBTree -variables {α : Type u} {β : Type v} {lt : α → α → Prop} +variables {α : Type u} {β : Type v} {lt : α → α → Bool} @[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat := RBMap.depth f t @@ -53,8 +53,6 @@ match RBMap.max t with instance [HasRepr α] : HasRepr (RBTree α lt) := ⟨λ t, "rbtreeOf " ++ repr t.toList⟩ -variables [DecidableRel lt] - @[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt := RBMap.insert t a () @@ -70,7 +68,7 @@ match RBMap.findCore t a with @[inline] def contains (t : RBTree α lt) (a : α) : Bool := (t.find a).isSome -def fromList (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt := +def fromList (l : List α) (lt : α → α → Bool) : RBTree α lt := l.foldl insert (mkRBTree α lt) @[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool := @@ -87,5 +85,5 @@ subset t₁ t₂ && subset t₂ t₁ end RBTree -def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt := +def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Bool) : RBTree α lt := RBTree.fromList l lt diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 7f87c4e65b..69e26a541c 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -54,17 +54,15 @@ open Parser.command open Parser.command.NotationSpec open Expander -local attribute [instance] Name.hasLtQuick - -- TODO(Sebastian): move /-- An RBMap that remembers the insertion order. -/ -structure OrderedRBMap (α β : Type) (lt : α → α → Prop) := +structure OrderedRBMap (α β : Type) (lt : α → α → Bool) := (entries : List (α × β)) (map : RBMap α (Nat × β) lt) (size : Nat) namespace OrderedRBMap -variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRBMap α β lt) +variables {α β : Type} {lt : α → α → Bool} (m : OrderedRBMap α β lt) def empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0} @@ -93,11 +91,11 @@ structure Scope := (notations : List NotationMacro := []) /- The set of local universe variables. We remember their insertion order so that we can keep the order when copying them to declarations. -/ -(univs : OrderedRBMap Name Level (<) := OrderedRBMap.empty) +(univs : OrderedRBMap Name Level Name.quickLt := OrderedRBMap.empty) /- The set of local variables. -/ -(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.empty) +(vars : OrderedRBMap Name SectionVar Name.quickLt := OrderedRBMap.empty) /- The subset of `vars` that is tagged as always included. -/ -(includeVars : RBTree Name (<) := mkRBTree _ _) +(includeVars : RBTree Name Name.quickLt := mkRBTree _ _) /- The stack of nested active `namespace` commands. -/ (nsStack : List Name := []) /- The set of active `open` declarations. -/ @@ -896,7 +894,7 @@ def eoi.elaborate : Elaborator := error cmd "invalid end of input, expected 'end'" -- TODO(Sebastian): replace with attribute -def elaborators : RBMap Name Elaborator (<) := RBMap.fromList [ +def elaborators : RBMap Name Elaborator Name.quickLt := RBMap.fromList [ (Module.header.name, Module.header.elaborate), (notation.name, notation.elaborate), (reserveNotation.name, reserveNotation.elaborate), diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index fdde771c85..c53599ba70 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -476,10 +476,8 @@ def universes.transform : transformer := def sorry.transform : transformer := λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.false] -local attribute [instance] Name.hasLtQuick - -- TODO(Sebastian): replace with attribute -def builtinTransformers : RBMap Name transformer (<) := RBMap.fromList [ +def builtinTransformers : RBMap Name transformer Name.quickLt := RBMap.fromList [ (mixfix.name, mixfix.transform), (reserveMixfix.name, reserveMixfix.transform), (bracketedBinders.name, bracketedBinders.transform), @@ -506,7 +504,7 @@ structure ExpanderState := (nextScope : MacroScope) structure ExpanderConfig extends TransformerConfig := -(transformers : RBMap Name transformer (<)) +(transformers : RBMap Name transformer Name.quickLt) instance ExpanderConfig.HasLift : HasLift ExpanderConfig TransformerConfig := ⟨ExpanderConfig.toTransformerConfig⟩ diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index a5b0338b53..2849620b5e 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -152,10 +152,9 @@ theorem mkNumeralNeMkNumeralOfNeNumeral (p₁ : Name) {n₁ : Nat} (p₂ : Name) end Name -local attribute [instance] Name.hasLtQuick -def NameMap (α : Type) := RBMap Name α (<) +def NameMap (α : Type) := RBMap Name α Name.quickLt -@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α (<) +@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickLt namespace NameMap variable {α : Type} @@ -172,9 +171,9 @@ def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n end NameMap -def NameSet := RBTree Name (<) +def NameSet := RBTree Name Name.quickLt -@[inline] def mkNameSet : NameSet := mkRBTree Name (<) +@[inline] def mkNameSet : NameSet := mkRBTree Name Name.quickLt namespace NameSet diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index a0f818c282..d540f3bd70 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -190,9 +190,8 @@ abbrev trailingTermParser := TrailingTermParserM Syntax instance trailingTermParserCoe : HasCoe termParser trailingTermParser := ⟨λ x _, x⟩ -local attribute [instance] Name.hasLtQuick /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/ -def TokenMap (α : Type) := RBMap Name (List α) (<) +def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt def TokenMap.insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α := match map.find k with diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 2750729b82..c83860cbdd 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -39,10 +39,10 @@ private partial def insertAux (s : String) (val : α) : Trie α → String.Pos | false := let c := s.get i in let i := s.next i in - let t := match RBNode.find (<) m c with + let t := match RBNode.find Char.lt m c with | none := insertEmptyAux s val i | some t := insertAux t i in - Trie.Node v (RBNode.insert (<) m c t) + Trie.Node v (RBNode.insert Char.lt m c t) def insert (t : Trie α) (s : String) (val : α) : Trie α := insertAux s val t 0 @@ -54,7 +54,7 @@ private partial def findAux (s : String) : Trie α → String.Pos → Option α | false := let c := s.get i in let i := s.next i in - match RBNode.find (<) m c with + match RBNode.find Char.lt m c with | none := none | some t := findAux t i @@ -74,7 +74,7 @@ private partial def matchPrefixAux (s : String) : Trie α → String.Pos → (St let acc := updtAcc v i acc in let c := s.get i in let i := s.next i in - match RBNode.find (<) m c with + match RBNode.find Char.lt m c with | some t := matchPrefixAux t i acc | none := acc @@ -86,7 +86,7 @@ private def oldMatchPrefixAux : Nat → Trie α → String.OldIterator → Optio | 0 (Trie.Node val map) it Acc := Prod.mk it <$> val <|> Acc | (n+1) (Trie.Node val map) it Acc := let Acc' := Prod.mk it <$> val <|> Acc in - match RBNode.find (<) map it.curr with + match RBNode.find Char.lt map it.curr with | some t := oldMatchPrefixAux n t it.next Acc' | none := Acc' diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean index e1a11aef34..da39fed833 100644 --- a/library/init/lean/position.lean +++ b/library/init/lean/position.lean @@ -20,14 +20,9 @@ instance : DecidableEq Position := else isFalse (λ contra, Position.noConfusion contra (λ e₁ e₂, absurd e₂ h₂)) else isFalse (λ contra, Position.noConfusion contra (λ e₁ e₂, absurd e₁ h₁))} -protected def lt : Position → Position → Prop +protected def lt : Position → Position → Bool | ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := (l₁, c₁) < (l₂, c₂) -instance : HasLess Position := ⟨Position.lt⟩ - -instance decidableLt : Π (p₁ p₂ : Position), Decidable (p₁ < p₂) -| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := inferInstanceAs $ Decidable ((l₁, c₁) < (l₂, c₂)) - instance : HasToFormat Position := ⟨λ ⟨l, c⟩, "⟨" ++ toFmt l ++ ", " ++ toFmt c ++ "⟩"⟩ @@ -37,7 +32,7 @@ end Position /-- A precomputed cache for quickly mapping Char offsets to positionitions. -/ structure FileMap := -- A mapping from Char offset of line start to line index -(lines : RBMap Nat Nat (<)) +(lines : RBMap Nat Nat (λ a b, a < b)) namespace FileMap private def fromStringAux : Nat → String.OldIterator → Nat → List (Nat × Nat) diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 340e577c13..d1966c9371 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -25,7 +25,7 @@ fmt ++ Format.nest 2 (Format.join $ subtraces.map (λ t, Format.line ++ t.pp)) namespace Trace -def TraceMap := RBMap Position Trace (<) +def TraceMap := RBMap Position Trace Position.lt structure TraceState := (opts : Options)