chore: update stage0

stage0/src/Init/Coe.lean

@@ -130,12 +130,12 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α :=
   coe := fun v => v.val
 }
 
-/- Coe & HasOfNat bridge -/
+/- Coe & OfNat bridge -/
 
 /-
-  Remark: one may question why we use `HasOfNat α` instead of `Coe Nat α`.
-  Reason: `HasOfNat` is for implementing polymorphic numeric literals, and we may
+  Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
+  Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
   want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
-instance hasOfNatOfCoe {α : Type u} {β : Type v} [HasOfNat α] [Coe α β] : HasOfNat β := {
-  ofNat := fun (n : Nat) => coe (HasOfNat.ofNat n : α)
+instance hasOfNatOfCoe {α : Type u} {β : Type v} [OfNat α] [Coe α β] : OfNat β := {
+  ofNat := fun (n : Nat) => coe (OfNat.ofNat n : α)
 }

stage0/src/Init/Control/Alternative.lean

@@ -12,7 +12,7 @@ class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1
   (failure : {α : Type u} → f α)
   (orelse  : {α : Type u} → f α → f α → f α)
 
-instance (f : Type u → Type v) (α : Type u) [Alternative f] : HasOrelse (f α) := ⟨Alternative.orelse⟩
+instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orelse⟩
 
 variables {f : Type u → Type v} [Alternative f] {α : Type u}
 

stage0/src/Init/Control/Applicative.lean

@@ -8,23 +8,11 @@ import Init.Control.Functor
 open Function
 universes u v
 
-class HasPure (f : Type u → Type v) :=
-  (pure {α : Type u} : α → f α)
-
-export HasPure (pure)
-
-class HasSeq (f : Type u → Type v) : Type (max (u+1) v) :=
-  (seq  : {α β : Type u} → f (α → β) → f α → f β)
-
-class HasSeqLeft (f : Type u → Type v) : Type (max (u+1) v) :=
-  (seqLeft : {α : Type u} → f α → f PUnit → f α)
-
-class HasSeqRight (f : Type u → Type v) : Type (max (u+1) v) :=
-  (seqRight : {β : Type u} → f PUnit → f β → f β)
-
 class Pure (f : Type u → Type v) :=
   (pure {α : Type u} : α → f α)
 
+export Pure (pure)
+
 class Seq (f : Type u → Type v) : Type (max (u+1) v) :=
   (seq  : {α β : Type u} → f (α → β) → f α → f β)
 
@@ -34,7 +22,7 @@ class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) :=
 class SeqRight (f : Type u → Type v) : Type (max (u+1) v) :=
   (seqRight : {β : Type u} → f PUnit → f β → f β)
 
-class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f, HasSeqLeft f, HasSeqRight f :=
+class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f :=
   (map      := fun x y => pure x <*> y)
   (seqLeft  := fun a b => const _ <$> a <*> b)
   (seqRight := fun a b => const _ id <$> a <*> b)

stage0/src/Init/Control/Conditional.lean

@@ -8,29 +8,26 @@ import Init.Control.Monad
 import Init.Data.Option.Basic
 universes u v
 
-class HasToBool (α : Type u) :=
-  (toBool : α → Bool)
-
 class ToBool (α : Type u) :=
   (toBool : α → Bool)
 
-export HasToBool (toBool)
+export ToBool (toBool)
 
-instance : HasToBool Bool := ⟨id⟩
-instance {α} : HasToBool (Option α) := ⟨Option.toBool⟩
+instance : ToBool Bool := ⟨id⟩
+instance {α} : ToBool (Option α) := ⟨Option.toBool⟩
 
-@[macroInline] def bool {β : Type u} {α : Type v} [HasToBool β] (f t : α) (b : β) : α :=
+@[macroInline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α :=
   match toBool b with
   | true  => t
   | false => f
 
-@[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do
+@[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
   | true  => pure b
   | false => y
 
-@[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do
+@[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
   let b ← x
   match toBool b with
   | true  => y

stage0/src/Init/Control/EState.lean

@@ -69,15 +69,15 @@ class Backtrackable (δ : outParam $ Type u) (σ : Type u) :=
   | Result.error e s => handle e (Backtrackable.restore s d)
   | ok               => ok
 
-@[inline] protected def orelse {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) : EStateM ε σ α := fun s =>
+@[inline] protected def orElse {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s;
   match x₁ s with
   | Result.error _ s => x₂ (Backtrackable.restore s d)
   | ok               => ok
 
-/-- Alternative orelse operator that allows to select which exception should be used.
-    The default is to use the first exception since the standard `orelse` uses the second. -/
-@[inline] protected def orelse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s =>
+/-- Alternative orElse operator that allows to select which exception should be used.
+    The default is to use the first exception since the standard `orElse` uses the second. -/
+@[inline] protected def orElse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s;
   match x₁ s with
   | Result.error e₁ s₁ =>
@@ -113,8 +113,8 @@ instance : Monad (EStateM ε σ) := {
   seqRight := EStateM.seqRight
 }
 
-instance {δ} [Backtrackable δ σ] : HasOrelse (EStateM ε σ α) := {
-  orelse := EStateM.orelse
+instance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) := {
+  orElse := EStateM.orElse
 }
 
 instance : MonadStateOf σ (EStateM ε σ) := {

stage0/src/Init/Control/Except.lean

@@ -171,7 +171,7 @@ variables {ε : Type u} {m : Type v → Type w}
 @[inline] protected def orelse [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
   tryCatch t₁ fun _ => t₂
 
-instance [MonadExcept ε m] {α : Type v} : HasOrelse (m α) := ⟨MonadExcept.orelse⟩
+instance [MonadExcept ε m] {α : Type v} : OrElse (m α) := ⟨MonadExcept.orelse⟩
 
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/

stage0/src/Init/Control/Id.lean

@@ -26,7 +26,7 @@ instance : Monad Id := {
 
 @[inline] protected def run {α : Type u} (x : Id α) : α := x
 
-instance {α} [HasOfNat α] : HasOfNat (Id α) :=
-inferInstanceAs (HasOfNat α)
+instance {α} [OfNat α] : OfNat (Id α) :=
+inferInstanceAs (OfNat α)
 
 end Id

stage0/src/Init/Control/Monad.lean

@@ -10,18 +10,15 @@ universes u v w
 
 open Function
 
-class HasBind (m : Type u → Type v) :=
-  (bind : {α β : Type u} → m α → (α → m β) → m β)
-
 class Bind (m : Type u → Type v) :=
   (bind : {α β : Type u} → m α → (α → m β) → m β)
 
-export HasBind (bind)
+export Bind (bind)
 
-@[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [HasBind m] (f : α → m β) (g : β → m δ) : α → m δ :=
+@[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [Bind m] (f : α → m β) (g : β → m δ) : α → m δ :=
   fun a => f a >>= g
 
-class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (u+1) v) :=
+class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) :=
   (map      := fun f x => x >>= pure ∘ f)
   (seq      := fun f x => f >>= (fun y => y <$> x))
   (seqLeft  := fun x y => x >>= fun a => y >>= fun _ => pure a)

stage0/src/Init/Control/MonadControl.lean

@@ -28,18 +28,18 @@ instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o := {
   restoreM := MonadControl.restoreM ∘ restoreM
 }
 
-instance (m : Type u → Type v) [HasPure m] : MonadControlT m m := {
+instance (m : Type u → Type v) [Pure m] : MonadControlT m m := {
   stM      := fun α => α,
   liftWith := fun f => f fun x => x,
   restoreM := fun x => pure x
 }
 
 @[inline]
-def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : HasBind n] {α : Type u}
+def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   liftWith f >>= restoreM
 
 @[inline]
-def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [HasBind n] {α : Type u}
+def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   controlAt m f

stage0/src/Init/Core.lean

@@ -270,15 +270,12 @@ inductive Nat
   | succ (n : Nat) : Nat
 
 /- For numeric literals notation -/
-class HasOfNat (α : Type u) :=
-  (ofNat : Nat → α)
-
-export HasOfNat (ofNat)
-
 class OfNat (α : Type u) :=
   (ofNat : Nat → α)
 
-instance : HasOfNat Nat := ⟨id⟩
+export OfNat (ofNat)
+
+instance : OfNat Nat := ⟨id⟩
 
 /- Auxiliary axiom used to implement `sorry`.
    TODO: add this theorem on-demand. That is,
@@ -286,23 +283,6 @@ instance : HasOfNat Nat := ⟨id⟩
 axiom sorryAx (α : Sort u) (synthetic := true) : α
 
 /- Declare builtin and reserved notation -/
-class HasAdd      (α : Type u) := (add : α → α → α)
-class HasMul      (α : Type u) := (mul : α → α → α)
-class HasNeg      (α : Type u) := (neg : α → α)
-class HasSub      (α : Type u) := (sub : α → α → α)
-class HasDiv      (α : Type u) := (div : α → α → α)
-class HasMod      (α : Type u) := (mod : α → α → α)
-class HasModN     (α : Type u) := (modn : α → Nat → α)
-class HasLessEq   (α : Type u) := (LessEq : α → α → Prop)
-class HasLess     (α : Type u) := (Less : α → α → Prop)
-class HasBeq      (α : Type u) := (beq : α → α → Bool)
-class HasAppend   (α : Type u) := (append : α → α → α)
-class HasOrelse   (α : Type u) := (orelse  : α → α → α)
-class HasAndthen  (α : Type u) := (andthen : α → α → α)
-class HasEquiv    (α : Sort u) := (Equiv : α → α → Prop)
-class HasEmptyc   (α : Type u) := (emptyc : α)
-class HasPow (α : Type u) (β : Type v) := (pow : α → β → α)
-
 class Add      (α : Type u) := (add : α → α → α)
 class Mul      (α : Type u) := (mul : α → α → α)
 class Neg      (α : Type u) := (neg : α → α)
@@ -312,7 +292,7 @@ class Mod      (α : Type u) := (mod : α → α → α)
 class ModN     (α : Type u) := (modn : α → Nat → α)
 class LessEq   (α : Type u) := (LessEq : α → α → Prop)
 class Less     (α : Type u) := (Less : α → α → Prop)
-class Beq      (α : Type u) := (beq : α → α → Bool)
+class BEq      (α : Type u) := (beq : α → α → Bool)
 class Append   (α : Type u) := (append : α → α → α)
 class OrElse   (α : Type u) := (orElse  : α → α → α)
 class AndThen  (α : Type u) := (andThen : α → α → α)
@@ -320,8 +300,8 @@ class Equiv    (α : Sort u) := (Equiv : α → α → Prop)
 class EmptyCollection (α : Type u) := (emptyCollection : α)
 class Pow (α : Type u) (β : Type v) := (pow : α → β → α)
 
-@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
-@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := HasLess.Less b a
+@[reducible] def GreaterEq {α : Type u} [LessEq α] (a b : α) : Prop := LessEq.LessEq b a
+@[reducible] def Greater {α : Type u} [Less α] (a b : α) : Prop     := Less.Less b a
 
 /- Nat basic instances -/
 
@@ -333,9 +313,9 @@ protected def Nat.add : (@& Nat) → (@& Nat) → Nat
 
 /- We mark the following definitions as pattern to make sure they can be used in recursive equations,
    and reduced by the equation Compiler. -/
-attribute [matchPattern] Nat.add HasAdd.add HasNeg.neg
+attribute [matchPattern] Nat.add Add.add Neg.neg
 
-instance : HasAdd Nat := ⟨Nat.add⟩
+instance : Add Nat := ⟨Nat.add⟩
 
 def std.priority.default : Nat := 1000
 def std.priority.max     : Nat := 0xFFFFFFFF
@@ -403,78 +383,75 @@ inductive PNonScalar : Type u
 
 /- sizeof -/
 
-class HasSizeof (α : Sort u) :=
-  (sizeof : α → Nat)
-
-export HasSizeof (sizeof)
-
 class SizeOf (α : Sort u) :=
   (sizeOf : α → Nat)
 
+export SizeOf (sizeOf)
+
 /-
-Declare sizeof instances and theorems for types declared before HasSizeof.
-From now on, the inductive Compiler will automatically generate sizeof instances and theorems.
+Declare sizeOf instances and theorems for types declared before SizeOf.
+From now on, the inductive Compiler will automatically generate sizeOf instances and theorems.
 -/
 
-/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/
-protected def default.sizeof (α : Sort u) : α → Nat
+/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/
+protected def default.sizeOf (α : Sort u) : α → Nat
   | a => 0
 
-instance (α : Sort u) : HasSizeof α :=
-  ⟨default.sizeof α⟩
+instance (α : Sort u) : SizeOf α :=
+  ⟨default.sizeOf α⟩
 
-instance : HasSizeof Nat := {
-  sizeof := fun n => n
+instance : SizeOf Nat := {
+  sizeOf := fun n => n
 }
 
-instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) := {
-  sizeof := fun (a, b) => 1 + sizeof a + sizeof b
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) := {
+  sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b
 }
 
-instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) := {
-  sizeof := fun
-    | Sum.inl a => 1 + sizeof a
-    | Sum.inr b => 1 + sizeof b
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) := {
+  sizeOf := fun
+    | Sum.inl a => 1 + sizeOf a
+    | Sum.inr b => 1 + sizeOf b
 }
 
-instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := {
-  sizeof := fun
-    | PSum.inl a => 1 + sizeof a
-    | PSum.inr b => 1 + sizeof b
+instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) := {
+  sizeOf := fun
+    | PSum.inl a => 1 + sizeOf a
+    | PSum.inr b => 1 + sizeOf b
 }
 
-instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) := {
-  sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b
+instance (α : Type u) (β : α → Type v) [SizeOf α] [∀ a, SizeOf (β a)] : SizeOf (Sigma β) := {
+  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
 }
 
-instance (α : Type u) (β : α → Type v) [HasSizeof α] [(a : α) → HasSizeof (β a)] : HasSizeof (PSigma β) := {
-  sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b
+instance (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) := {
+  sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b
 }
 
-instance : HasSizeof PUnit := {
-  sizeof := fun _ => 1
+instance : SizeOf PUnit := {
+  sizeOf := fun _ => 1
 }
 
-instance : HasSizeof Bool := {
-  sizeof := fun _ => 1
+instance : SizeOf Bool := {
+  sizeOf := fun _ => 1
 }
 
-instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) := {
-  sizeof := fun
+instance (α : Type u) [SizeOf α] : SizeOf (Option α) := {
+  sizeOf := fun
     | none   => 1
-    | some a => 1 + sizeof a
+    | some a => 1 + sizeOf a
 }
 
-instance (α : Type u) [HasSizeof α] : HasSizeof (List α) := {
-  sizeof := fun as =>
+instance (α : Type u) [SizeOf α] : SizeOf (List α) := {
+  sizeOf := fun as =>
     let rec loop
       | List.nil      => 1
-      | List.cons x xs => 1 + sizeof x + loop xs
+      | List.cons x xs => 1 + sizeOf x + loop xs
     loop as
 }
 
-instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) := {
-  sizeof := fun ⟨a, _⟩ => sizeof a
+instance {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) := {
+  sizeOf := fun ⟨a, _⟩ => sizeOf a
 }
 
 theorem natAddZero (n : Nat) : n + 0 = n := rfl
@@ -513,7 +490,7 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf
 @[extern c inline "#1 || #2"] def strictOr  (b₁ b₂ : Bool) := b₁ || b₂
 @[extern c inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂
 
-@[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
+@[inline] def bne {α : Type u} [BEq α] (a b : α) : Bool :=
   !(a == b)
 
 /- Logical connectives an equality -/
@@ -792,7 +769,7 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 export Decidable (isTrue isFalse decide)
 
-instance {α : Type u} [DecidableEq α] : HasBeq α :=
+instance {α : Type u} [DecidableEq α] : BEq α :=
   ⟨fun a b => decide (a = b)⟩
 
 theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
@@ -1273,21 +1250,21 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
       | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
     | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))
 
-instance [HasBeq α] [HasBeq β] : HasBeq (α × β) := {
+instance [BEq α] [BEq β] : BEq (α × β) := {
   beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂
 }
 
-instance [HasLess α] [HasLess β] : HasLess (α × β) := {
+instance [Less α] [Less β] : Less (α × β) := {
   Less := fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
 }
 
 instance prodHasDecidableLt
-         [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β]
+         [Less α] [Less β] [DecidableEq α] [DecidableEq β]
          [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
          : (s t : α × β) → Decidable (s < t) :=
   fun t s => inferInstanceAs (Decidable (_ ∨ _))
 
-theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
+theorem Prod.ltDef [Less α] [Less β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
   rfl
 end
 
@@ -1330,7 +1307,7 @@ class Setoid (α : Sort u) :=
   (r : α → α → Prop)
   (iseqv {} : Equivalence r)
 
-instance {α : Sort u} [Setoid α] : HasEquiv α :=
+instance {α : Sort u} [Setoid α] : Equiv α :=
   ⟨Setoid.r⟩
 
 namespace Setoid

stage0/src/Init/Data/Array/Basic.lean

@@ -59,7 +59,7 @@ theorem szMkArrayEq (n : Nat) (v : α) : (mkArray n v).sz = n :=
 def empty : Array α :=
   mkEmpty 0
 
-instance : HasEmptyc (Array α) := ⟨Array.empty⟩
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
 instance : Inhabited (Array α) := ⟨Array.empty⟩
 
 def isEmpty (a : Array α) : Bool :=
@@ -324,7 +324,7 @@ match findIdxAux a p 0 with
 | some i => i
 | none   => panic! "failed to find element"
 
-def getIdx? [HasBeq α] (a : Array α) (v : α) : Option Nat :=
+def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 a.findIdx? $ fun a => a == v
 
 end
@@ -541,7 +541,7 @@ end
 protected def append (a : Array α) (b : Array α) : Array α :=
 b.foldl (fun a v => a.push v) a
 
-instance : HasAppend (Array α) := ⟨Array.append⟩
+instance : Append (Array α) := ⟨Array.append⟩
 
 -- TODO(Leo): justify termination using wf-rec
 @[specialize] partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) : Nat → Bool
@@ -561,8 +561,8 @@ if h : a.size = b.size then
 else
   false
 
-instance [HasBeq α] : HasBeq (Array α) :=
-⟨fun a b => isEqv a b HasBeq.beq⟩
+instance [BEq α] : BEq (Array α) :=
+⟨fun a b => isEqv a b BEq.beq⟩
 
 -- TODO(Leo): justify termination using wf-rec, and use `swap`
 partial def reverseAux : Array α → Nat → Array α
@@ -628,7 +628,7 @@ filterMapMAux f as 0 Array.empty
 @[inline] def filterMap {α β : Type u} (f : α → Option β) (as : Array α) : Array β :=
 Id.run $ filterMapM f as
 
-partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option (Fin a.size)
+partial def indexOfAux {α} [BEq α] (a : Array α) (v : α) : Nat → Option (Fin a.size)
 | i =>
   if h : i < a.size then
     let idx : Fin a.size := ⟨i, h⟩;
@@ -636,7 +636,7 @@ partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option
     else indexOfAux a v (i+1)
   else none
 
-def indexOf? {α} [HasBeq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+def indexOf? {α} [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
 indexOfAux a v 0
 
 partial def eraseIdxAux {α} : Nat → Array α → Array α
@@ -679,13 +679,13 @@ end
 def eraseIdx' {α} (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
 eraseIdxSzAux a (i.val + 1) a rfl
 
-def contains [HasBeq α] (as : Array α) (a : α) : Bool :=
+def contains [BEq α] (as : Array α) (a : α) : Bool :=
 as.any $ fun b => a == b
 
-def elem [HasBeq α] (a : α) (as : Array α) : Bool :=
+def elem [BEq α] (a : α) (as : Array α) : Bool :=
 as.contains a
 
-def erase [HasBeq α] (as : Array α) (a : α) : Array α :=
+def erase [BEq α] (as : Array α) (a : α) : Array α :=
 match as.indexOf? a with
 | none   => as
 | some i => as.feraseIdx i
@@ -807,7 +807,7 @@ else
 @[inline] def partition {α : Type u} (p : α → Bool) (as : Array α) : Array α × Array α :=
 partitionAux p as 0 #[] #[]
 
-partial def isPrefixOfAux {α : Type u} [HasBeq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool
+partial def isPrefixOfAux {α : Type u} [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool
 | i =>
   if h : i < as.size then
     let a := as.get ⟨i, h⟩;
@@ -820,26 +820,26 @@ partial def isPrefixOfAux {α : Type u} [HasBeq α] (as bs : Array α) (hle : as
     true
 
 /- Return true iff `as` is a prefix of `bs` -/
-def isPrefixOf  {α : Type u} [HasBeq α] (as bs : Array α) : Bool :=
+def isPrefixOf  {α : Type u} [BEq α] (as bs : Array α) : Bool :=
 if h : as.size ≤ bs.size then
   isPrefixOfAux as bs h 0
 else
   false
 
-private def allDiffAuxAux {α} [HasBeq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+private def allDiffAuxAux {α} [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
 | 0,   h => true
 | i+1, h =>
   have i < as.size from Nat.ltTrans (Nat.ltSuccSelf _) h;
   a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this
 
-private partial def allDiffAux {α} [HasBeq α] (as : Array α) : Nat → Bool
+private partial def allDiffAux {α} [BEq α] (as : Array α) : Nat → Bool
 | i =>
   if h : i < as.size then
     allDiffAuxAux as (as.get ⟨i, h⟩) i h && allDiffAux as (i+1)
   else
     true
 
-def allDiff {α} [HasBeq α] (as : Array α) : Bool :=
+def allDiff {α} [BEq α] (as : Array α) : Bool :=
 allDiffAux as 0
 
 @[specialize] partial def zipWithAux {α β γ} (f : α → β → γ) (as : Array α) (bs : Array β) : Nat → Array γ → Array γ

stage0/src/Init/Data/ByteArray/Basic.lean

@@ -58,7 +58,7 @@ protected def append (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
   b.copySlice 0 a a.size b.size false
 
-instance : HasAppend ByteArray := ⟨ByteArray.append⟩
+instance : Append ByteArray := ⟨ByteArray.append⟩
 
 partial def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=

stage0/src/Init/Data/Char/Basic.lean

@@ -15,7 +15,7 @@ structure Char :=
   (val : UInt32)
   (valid : isValidChar val)
 
-instance : HasSizeof Char := ⟨fun c => c.val.toNat⟩
+instance : SizeOf Char := ⟨fun c => c.val.toNat⟩
 
 namespace Char
 def utf8Size (c : Char) : UInt32 :=
@@ -28,8 +28,8 @@ def utf8Size (c : Char) : UInt32 :=
 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.Less⟩
-instance : HasLessEq Char := ⟨Char.LessEq⟩
+instance : Less Char   := ⟨Char.Less⟩
+instance : LessEq Char := ⟨Char.LessEq⟩
 
 protected def lt (a b : Char) : Bool := a.val < b.val
 

stage0/src/Init/Data/Fin/Basic.lean

@@ -24,8 +24,8 @@ protected def lt {n} (a b : Fin n) : Prop :=
 protected def le {n} (a b : Fin n) : Prop :=
   a.val ≤ b.val
 
-instance {n} : HasLess (Fin n)    := ⟨Fin.lt⟩
-instance {n} : HasLessEq (Fin n)  := ⟨Fin.le⟩
+instance {n} : Less (Fin n)    := ⟨Fin.lt⟩
+instance {n} : LessEq (Fin n)  := ⟨Fin.le⟩
 
 instance decLt {n} (a b : Fin n) :  Decidable (a < b) :=
   Nat.decLt ..
@@ -80,12 +80,12 @@ def land : Fin n → Fin n → Fin n
 def lor : Fin n → Fin n → Fin n
   | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
 
-instance : HasAdd (Fin n)         := ⟨Fin.add⟩
-instance : HasSub (Fin n)         := ⟨Fin.sub⟩
-instance : HasMul (Fin n)         := ⟨Fin.mul⟩
-instance : HasMod (Fin n)         := ⟨Fin.mod⟩
-instance : HasDiv (Fin n)         := ⟨Fin.div⟩
-instance : HasModN (Fin n)        := ⟨Fin.modn⟩
+instance : Add (Fin n)         := ⟨Fin.add⟩
+instance : Sub (Fin n)         := ⟨Fin.sub⟩
+instance : Mul (Fin n)         := ⟨Fin.mul⟩
+instance : Mod (Fin n)         := ⟨Fin.mod⟩
+instance : Div (Fin n)         := ⟨Fin.div⟩
+instance : ModN (Fin n)        := ⟨Fin.modn⟩
 
 theorem eqOfVeq : ∀ {i j : Fin n}, (val i) = (val j) → i = j
   | ⟨iv, ilt₁⟩, ⟨_, _⟩, rfl => rfl

stage0/src/Init/Data/Float.lean

@@ -44,17 +44,17 @@ def Float.lt  : Float → Float → Prop := fun a b =>
 def Float.le  : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
-instance : HasOfNat Float  := ⟨Float.ofNat⟩
-instance : HasAdd Float    := ⟨Float.add⟩
-instance : HasSub Float    := ⟨Float.sub⟩
-instance : HasMul Float    := ⟨Float.mul⟩
-instance : HasDiv Float    := ⟨Float.div⟩
-instance : HasLess Float   := ⟨Float.lt⟩
-instance : HasLessEq Float := ⟨Float.le⟩
+instance : OfNat Float  := ⟨Float.ofNat⟩
+instance : Add Float    := ⟨Float.add⟩
+instance : Sub Float    := ⟨Float.sub⟩
+instance : Mul Float    := ⟨Float.mul⟩
+instance : Div Float    := ⟨Float.div⟩
+instance : Less Float   := ⟨Float.lt⟩
+instance : LessEq Float := ⟨Float.le⟩
 
 @[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool
 
-instance : HasBeq Float := ⟨Float.beq⟩
+instance : BEq Float := ⟨Float.beq⟩
 
 @[extern c inline "#1 < #2"]   constant Float.decLt (a b : Float) : Decidable (a < b) :=
   match a, b with
@@ -96,4 +96,4 @@ abbrev Nat.toFloat (n : Nat) : Float :=
 @[extern "sqrt"] constant Float.sqrt : Float → Float
 @[extern "cbrt"] constant Float.cbrt : Float → Float
 
-instance : HasPow Float Float := ⟨Float.pow⟩
+instance : Pow Float Float := ⟨Float.pow⟩

stage0/src/Init/Data/Int/Basic.lean

@@ -60,26 +60,26 @@ protected def mul (m n : @& Int) : Int :=
   | negSucc m, ofNat n   => negOfNat (succ m * n)
   | negSucc m, negSucc n => ofNat (succ m * succ n)
 
-instance : HasNeg Int := ⟨Int.neg⟩
-instance : HasAdd Int := ⟨Int.add⟩
-instance : HasMul Int := ⟨Int.mul⟩
+instance : Neg Int := ⟨Int.neg⟩
+instance : Add Int := ⟨Int.add⟩
+instance : Mul Int := ⟨Int.mul⟩
 
 @[extern "lean_int_sub"]
 protected def sub (m n : @& Int) : Int :=
   m + (- n)
 
-instance : HasSub Int := ⟨Int.sub⟩
+instance : Sub Int := ⟨Int.sub⟩
 
 inductive NonNeg : Int → Prop
   | mk (n : Nat) : NonNeg (ofNat n)
 
 protected def LessEq (a b : Int) : Prop := NonNeg (b - a)
 
-instance : HasLessEq Int := ⟨Int.LessEq⟩
+instance : LessEq Int := ⟨Int.LessEq⟩
 
 protected def Less (a b : Int) : Prop := (a + 1) ≤ b
 
-instance : HasLess Int := ⟨Int.Less⟩
+instance : Less Int := ⟨Int.Less⟩
 
 set_option bootstrap.gen_matcher_code false in
 @[extern "lean_int_dec_eq"]
@@ -124,7 +124,7 @@ protected def repr : Int → String
 
 instance : Repr Int := ⟨Int.repr⟩
 instance : ToString Int := ⟨Int.repr⟩
-instance : HasOfNat Int := ⟨Int.ofNat⟩
+instance : OfNat Int := ⟨Int.ofNat⟩
 
 @[extern "lean_int_div"]
 def div : (@& Int) → (@& Int) → Int
@@ -140,8 +140,8 @@ def mod : (@& Int) → (@& Int) → Int
   | negSucc m, ofNat n   => -ofNat (succ m % n)
   | negSucc m, negSucc n => -ofNat (succ m % succ n)
 
-instance : HasDiv Int := ⟨Int.div⟩
-instance : HasMod Int := ⟨Int.mod⟩
+instance : Div Int := ⟨Int.div⟩
+instance : Mod Int := ⟨Int.mod⟩
 
 def toNat : Int → Nat
   | ofNat n   => n

stage0/src/Init/Data/List/Basic.lean

@@ -40,7 +40,7 @@ def reverse (as : List α) :List α :=
 protected def append (as bs : List α) : List α :=
   reverseAux as.reverse bs
 
-instance : HasAppend (List α) := ⟨List.append⟩
+instance : Append (List α) := ⟨List.append⟩
 
 theorem reverseAuxReverseAuxNil : ∀ (as bs : List α), reverseAux (reverseAux as bs) [] = reverseAux bs as
   | [], bs     => rfl
@@ -70,9 +70,9 @@ theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++
     rw [consAppend, consAppend, appendAssoc, consAppend]
     exact rfl
 
-instance : HasEmptyc (List α) := ⟨List.nil⟩
+instance : EmptyCollection (List α) := ⟨List.nil⟩
 
-protected def erase {α} [HasBeq α] : List α → α → List α
+protected def erase {α} [BEq α] : List α → α → List α
   | [],    b => []
   | a::as, b => match a == b with
     | true  => as
@@ -156,41 +156,41 @@ def findSome? (f : α → Option β) : List α → Option β
     | some b => some b
     | none   => findSome? f as
 
-def replace [HasBeq α] : List α → α → α → List α
+def replace [BEq α] : List α → α → α → List α
   | [],    _, _ => []
   | a::as, b, c => match a == b with
     | true  => c::as
     | flase => a :: (replace as b c)
 
-def elem [HasBeq α] (a : α) : List α → Bool
+def elem [BEq α] (a : α) : List α → Bool
   | []    => false
   | b::bs => match a == b with
     | true  => true
     | false => elem a bs
 
-def notElem [HasBeq α] (a : α) (as : List α) : Bool :=
+def notElem [BEq α] (a : α) (as : List α) : Bool :=
   !(as.elem a)
 
-abbrev contains [HasBeq α] (as : List α) (a : α) : Bool :=
+abbrev contains [BEq α] (as : List α) (a : α) : Bool :=
   elem a as
 
-def eraseDupsAux {α} [HasBeq α] : List α → List α → List α
+def eraseDupsAux {α} [BEq α] : List α → List α → List α
   | [],    bs => bs.reverse
   | a::as, bs => match bs.elem a with
     | true  => eraseDupsAux as bs
     | false => eraseDupsAux as (a::bs)
 
-def eraseDups {α} [HasBeq α] (as : List α) : List α :=
+def eraseDups {α} [BEq α] (as : List α) : List α :=
   eraseDupsAux as []
 
-def eraseRepsAux {α} [HasBeq α] : α → List α → List α → List α
+def eraseRepsAux {α} [BEq α] : α → List α → List α → List α
   | a, [], rs => (a::rs).reverse
   | a, a'::as, rs => match a == a' with
     | true  => eraseRepsAux a as rs
     | false => eraseRepsAux a' as (a::rs)
 
 /-- Erase repeated adjacent elements. -/
-def eraseReps {α} [HasBeq α] : List α → List α
+def eraseReps {α} [BEq α] : List α → List α
   | []    => []
   | a::as => eraseRepsAux a as []
 
@@ -213,13 +213,13 @@ def eraseReps {α} [HasBeq α] : List α → List α
   | []    => []
   | a::as => groupByAux p as [[a]]
 
-def lookup [HasBeq α] : α → List (α × β) → Option β
+def lookup [BEq α] : α → List (α × β) → Option β
   | _, []        => none
   | a, (k,b)::es => match a == k with
     | true  => some b
     | false => lookup a es
 
-def removeAll [HasBeq α] (xs ys : List α) : List α :=
+def removeAll [BEq α] (xs ys : List α) : List α :=
   xs.filter (fun x => ys.notElem x)
 
 def drop : Nat → List α → List α
@@ -298,47 +298,47 @@ def intercalate (sep : List α) (xs : List (List α)) : List α :=
 
 @[inline] protected def pure {α : Type u} (a : α) : List α := [a]
 
-inductive Less [HasLess α] : List α → List α → Prop
+inductive List.Less [Less α] : List α → List α → Prop
   | nil  (b : α) (bs : List α) : Less [] (b::bs)
   | head {a : α} (as : List α) {b : α} (bs : List α) : a < b → Less (a::as) (b::bs)
   | tail {a : α} {as : List α} {b : α} {bs : List α} : ¬ a < b → ¬ b < a → Less as bs → Less (a::as) (b::bs)
 
-instance less [HasLess α] : HasLess (List α) := ⟨List.Less⟩
+instance less [Less α] : Less (List α) := ⟨List.Less⟩
 
-instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
+instance hasDecidableLt [Less α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
   | [],    []    => isFalse (fun h => nomatch h)
-  | [],    b::bs => isTrue (Less.nil _ _)
+  | [],    b::bs => isTrue (List.Less.nil _ _)
   | a::as, []    => isFalse (fun h => nomatch h)
   | a::as, b::bs =>
     match h a b with
-    | isTrue h₁  => isTrue (Less.head _ _ h₁)
+    | isTrue h₁  => isTrue (List.Less.head _ _ h₁)
     | isFalse h₁ =>
       match h b a with
       | isTrue h₂  => isFalse (fun h => match h with
-         | Less.head _ _ h₁' => absurd h₁' h₁
-         | Less.tail _ h₂' _ => absurd h₂ h₂')
+         | List.Less.head _ _ h₁' => absurd h₁' h₁
+         | List.Less.tail _ h₂' _ => absurd h₂ h₂')
       | isFalse h₂ =>
         match hasDecidableLt as bs with
-        | isTrue h₃  => isTrue (Less.tail h₁ h₂ h₃)
+        | isTrue h₃  => isTrue (List.Less.tail h₁ h₂ h₃)
         | isFalse h₃ => isFalse (fun h => match h with
-           | Less.head _ _ h₁' => absurd h₁' h₁
-           | Less.tail _ _ h₃' => absurd h₃' h₃)
+           | List.Less.head _ _ h₁' => absurd h₁' h₁
+           | List.Less.tail _ _ h₃' => absurd h₃' h₃)
 
-@[reducible] protected def LessEq [HasLess α] (a b : List α) : Prop := ¬ b < a
+@[reducible] protected def LessEq [Less α] (a b : List α) : Prop := ¬ b < a
 
-instance lessEq [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩
+instance lessEq [Less α] : LessEq (List α) := ⟨List.LessEq⟩
 
-instance [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
+instance [Less α] [h : DecidableRel (Less.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
   fun a b => inferInstanceAs (Decidable (Not _))
 
 /--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/
-def isPrefixOf [HasBeq α] : List α → List α → Bool
+def isPrefixOf [BEq α] : List α → List α → Bool
   | [],    _     => true
   | _,     []    => false
   | a::as, b::bs => a == b && isPrefixOf as bs
 
 /--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/
-def isSuffixOf [HasBeq α] (l₁ l₂ : List α) : Bool :=
+def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
 @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool
@@ -346,11 +346,11 @@ def isSuffixOf [HasBeq α] (l₁ l₂ : List α) : Bool :=
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
   | _,     _,     eqv => false
 
-protected def beq [HasBeq α] : List α → List α → Bool
+protected def beq [BEq α] : List α → List α → Bool
   | [],    []    => true
   | a::as, b::bs => a == b && List.beq as bs
   | _,     _     => false
 
-instance [HasBeq α] : HasBeq (List α) := ⟨List.beq⟩
+instance [BEq α] : BEq (List α) := ⟨List.beq⟩
 
 end List

stage0/src/Init/Data/Nat/Basic.lean

@@ -53,12 +53,12 @@ def ble : Nat → Nat → Bool
 protected def le (n m : Nat) : Prop :=
   ble n m = true
 
-instance : HasLessEq Nat := ⟨Nat.le⟩
+instance : LessEq Nat := ⟨Nat.le⟩
 
 protected def lt (n m : Nat) : Prop :=
   Nat.le (succ n) m
 
-instance : HasLess Nat := ⟨Nat.lt⟩
+instance : Less Nat := ⟨Nat.lt⟩
 
 set_option bootstrap.gen_matcher_code false in
 @[extern c inline "lean_nat_sub(#1, lean_box(1))"]
@@ -78,8 +78,8 @@ protected def mul : (@& Nat) → (@& Nat) → Nat
   | a, 0   => 0
   | a, b+1 => (Nat.mul a b) + a
 
-instance : HasSub Nat := ⟨Nat.sub⟩
-instance : HasMul Nat := ⟨Nat.mul⟩
+instance : Sub Nat := ⟨Nat.sub⟩
+instance : Mul Nat := ⟨Nat.mul⟩
 
 @[specialize] def foldAux {α : Type u} (f : Nat → α → α) (s : Nat) : Nat → α → α
   | 0,      a => a
@@ -117,7 +117,7 @@ protected def pow (m : @& Nat) : (@& Nat) → Nat
   | 0      => 1
   | succ n => Nat.pow m n * m
 
-instance : HasPow Nat Nat := ⟨Nat.pow⟩
+instance : Pow Nat Nat := ⟨Nat.pow⟩
 
 /- Nat.add theorems -/
 
@@ -444,7 +444,7 @@ theorem leAddLeft (n m : Nat): n ≤ m + n :=
 
 theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
   | zero,   zero,   h => ⟨0, rfl⟩
-  | zero,   succ n, h => ⟨succ n, show 0 + succ n = succ n from (Nat.addComm 0 (succ n)).symm ▸ rfl⟩
+  | zero,   succ n, h => ⟨succ n, Nat.addComm 0 (succ n) ▸ rfl⟩
   | succ n, zero,   h => Bool.noConfusion h
   | succ n, succ m, h =>
     have n ≤ m from h

stage0/src/Init/Data/Nat/Div.lean

@@ -18,7 +18,7 @@ private def div.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) :
 protected def div (a b : @& Nat) : Nat :=
   WellFounded.fix ltWf div.F a b
 
-instance : HasDiv Nat := ⟨Nat.div⟩
+instance : Div Nat := ⟨Nat.div⟩
 
 private theorem divDefAux (x y : Nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
   congrFun (WellFounded.fixEq ltWf div.F x) y
@@ -49,7 +49,7 @@ private def mod.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) :
 protected def mod (a b : @& Nat) : Nat :=
   WellFounded.fix ltWf mod.F a b
 
-instance : HasMod Nat := ⟨Nat.mod⟩
+instance : Mod Nat := ⟨Nat.mod⟩
 
 private theorem modDefAux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x :=
   congrFun (WellFounded.fixEq ltWf mod.F x) y

stage0/src/Init/Data/Option/Basic.lean

@@ -98,11 +98,11 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) := fun a b =>
     | (isTrue e)  => isTrue (congrArg (@some α) e)
     | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))
 
-instance {α : Type u} [HasBeq α] : HasBeq (Option α) := ⟨fun a b =>
+instance {α : Type u} [BEq α] : BEq (Option α) := ⟨fun a b =>
   match a, b with
   | none,      none      => true
   | none,      (some v₂) => false
   | (some v₁), none      => false
   | (some v₁), (some v₂) => v₁ == v₂⟩
 
-instance {α : Type u} [HasLess α] : HasLess (Option α) := ⟨Option.lt HasLess.Less⟩
+instance {α : Type u} [Less α] : Less (Option α) := ⟨Option.lt Less.Less⟩

stage0/src/Init/Data/String/Basic.lean

@@ -40,7 +40,7 @@ def List.asString (s : List Char) : String :=
   ⟨s⟩
 
 namespace String
-instance : HasLess String :=
+instance : Less String :=
   ⟨fun s₁ s₂ => s₁.data < s₂.data⟩
 
 @[extern "lean_string_dec_lt"]
@@ -197,9 +197,9 @@ def splitOn (s : String) (sep : String := " ") : List String :=
 
 instance : Inhabited String := ⟨""⟩
 
-instance : HasSizeof String := ⟨String.length⟩
+instance : SizeOf String := ⟨String.length⟩
 
-instance : HasAppend String := ⟨String.append⟩
+instance : Append String := ⟨String.append⟩
 
 def str : String → Char → String := push
 
@@ -508,7 +508,7 @@ def toNat? (s : Substring) : Option Nat :=
 def beq (ss1 ss2 : Substring) : Bool :=
   ss1.toString == ss2.toString
 
-instance hasBeq : HasBeq Substring := ⟨beq⟩
+instance hasBeq : BEq Substring := ⟨beq⟩
 
 end Substring
 

stage0/src/Init/Data/UInt.lean

@@ -37,15 +37,15 @@ def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
-instance : HasOfNat UInt8    := ⟨UInt8.ofNat⟩
-instance : HasAdd UInt8      := ⟨UInt8.add⟩
-instance : HasSub UInt8      := ⟨UInt8.sub⟩
-instance : HasMul UInt8      := ⟨UInt8.mul⟩
-instance : HasMod UInt8      := ⟨UInt8.mod⟩
-instance : HasModN UInt8     := ⟨UInt8.modn⟩
-instance : HasDiv UInt8      := ⟨UInt8.div⟩
-instance : HasLess UInt8     := ⟨UInt8.lt⟩
-instance : HasLessEq UInt8   := ⟨UInt8.le⟩
+instance : OfNat UInt8    := ⟨UInt8.ofNat⟩
+instance : Add UInt8      := ⟨UInt8.add⟩
+instance : Sub UInt8      := ⟨UInt8.sub⟩
+instance : Mul UInt8      := ⟨UInt8.mul⟩
+instance : Mod UInt8      := ⟨UInt8.mod⟩
+instance : ModN UInt8     := ⟨UInt8.modn⟩
+instance : Div UInt8      := ⟨UInt8.div⟩
+instance : Less UInt8     := ⟨UInt8.lt⟩
+instance : LessEq UInt8   := ⟨UInt8.le⟩
 instance : Inhabited UInt8   := ⟨0⟩
 
 set_option bootstrap.gen_matcher_code false in
@@ -99,15 +99,15 @@ def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
 
-instance : HasOfNat UInt16    := ⟨UInt16.ofNat⟩
-instance : HasAdd UInt16      := ⟨UInt16.add⟩
-instance : HasSub UInt16      := ⟨UInt16.sub⟩
-instance : HasMul UInt16      := ⟨UInt16.mul⟩
-instance : HasMod UInt16      := ⟨UInt16.mod⟩
-instance : HasModN UInt16     := ⟨UInt16.modn⟩
-instance : HasDiv UInt16      := ⟨UInt16.div⟩
-instance : HasLess UInt16     := ⟨UInt16.lt⟩
-instance : HasLessEq UInt16   := ⟨UInt16.le⟩
+instance : OfNat UInt16    := ⟨UInt16.ofNat⟩
+instance : Add UInt16      := ⟨UInt16.add⟩
+instance : Sub UInt16      := ⟨UInt16.sub⟩
+instance : Mul UInt16      := ⟨UInt16.mul⟩
+instance : Mod UInt16      := ⟨UInt16.mod⟩
+instance : ModN UInt16     := ⟨UInt16.modn⟩
+instance : Div UInt16      := ⟨UInt16.div⟩
+instance : Less UInt16     := ⟨UInt16.lt⟩
+instance : LessEq UInt16   := ⟨UInt16.le⟩
 instance : Inhabited UInt16   := ⟨0⟩
 
 set_option bootstrap.gen_matcher_code false in
@@ -168,15 +168,15 @@ def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
 @[extern c inline "((uint32_t)#1)"]
 def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
 
-instance : HasOfNat UInt32    := ⟨UInt32.ofNat⟩
-instance : HasAdd UInt32      := ⟨UInt32.add⟩
-instance : HasSub UInt32      := ⟨UInt32.sub⟩
-instance : HasMul UInt32      := ⟨UInt32.mul⟩
-instance : HasMod UInt32      := ⟨UInt32.mod⟩
-instance : HasModN UInt32     := ⟨UInt32.modn⟩
-instance : HasDiv UInt32      := ⟨UInt32.div⟩
-instance : HasLess UInt32     := ⟨UInt32.lt⟩
-instance : HasLessEq UInt32   := ⟨UInt32.le⟩
+instance : OfNat UInt32    := ⟨UInt32.ofNat⟩
+instance : Add UInt32      := ⟨UInt32.add⟩
+instance : Sub UInt32      := ⟨UInt32.sub⟩
+instance : Mul UInt32      := ⟨UInt32.mul⟩
+instance : Mod UInt32      := ⟨UInt32.mod⟩
+instance : ModN UInt32     := ⟨UInt32.modn⟩
+instance : Div UInt32      := ⟨UInt32.div⟩
+instance : Less UInt32     := ⟨UInt32.lt⟩
+instance : LessEq UInt32   := ⟨UInt32.le⟩
 instance : Inhabited UInt32   := ⟨0⟩
 
 set_option bootstrap.gen_matcher_code false in
@@ -248,15 +248,15 @@ constant UInt64.shiftLeft (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
 @[extern c inline "#1 >> #2"]
 constant UInt64.shiftRight (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
 
-instance : HasOfNat UInt64    := ⟨UInt64.ofNat⟩
-instance : HasAdd UInt64      := ⟨UInt64.add⟩
-instance : HasSub UInt64      := ⟨UInt64.sub⟩
-instance : HasMul UInt64      := ⟨UInt64.mul⟩
-instance : HasMod UInt64      := ⟨UInt64.mod⟩
-instance : HasModN UInt64     := ⟨UInt64.modn⟩
-instance : HasDiv UInt64      := ⟨UInt64.div⟩
-instance : HasLess UInt64     := ⟨UInt64.lt⟩
-instance : HasLessEq UInt64   := ⟨UInt64.le⟩
+instance : OfNat UInt64    := ⟨UInt64.ofNat⟩
+instance : Add UInt64      := ⟨UInt64.add⟩
+instance : Sub UInt64      := ⟨UInt64.sub⟩
+instance : Mul UInt64      := ⟨UInt64.mul⟩
+instance : Mod UInt64      := ⟨UInt64.mod⟩
+instance : ModN UInt64     := ⟨UInt64.modn⟩
+instance : Div UInt64      := ⟨UInt64.div⟩
+instance : Less UInt64     := ⟨UInt64.lt⟩
+instance : LessEq UInt64   := ⟨UInt64.le⟩
 instance : Inhabited UInt64   := ⟨0⟩
 
 @[extern c inline "(uint64_t)#1"]
@@ -327,15 +327,15 @@ constant USize.shiftRight (a b : USize) : USize := (arbitrary Nat).toUSize
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
-instance : HasOfNat USize    := ⟨USize.ofNat⟩
-instance : HasAdd USize      := ⟨USize.add⟩
-instance : HasSub USize      := ⟨USize.sub⟩
-instance : HasMul USize      := ⟨USize.mul⟩
-instance : HasMod USize      := ⟨USize.mod⟩
-instance : HasModN USize     := ⟨USize.modn⟩
-instance : HasDiv USize      := ⟨USize.div⟩
-instance : HasLess USize     := ⟨USize.lt⟩
-instance : HasLessEq USize   := ⟨USize.le⟩
+instance : OfNat USize    := ⟨USize.ofNat⟩
+instance : Add USize      := ⟨USize.add⟩
+instance : Sub USize      := ⟨USize.sub⟩
+instance : Mul USize      := ⟨USize.mul⟩
+instance : Mod USize      := ⟨USize.mod⟩
+instance : ModN USize     := ⟨USize.modn⟩
+instance : Div USize      := ⟨USize.div⟩
+instance : Less USize     := ⟨USize.lt⟩
+instance : LessEq USize   := ⟨USize.le⟩
 instance : Inhabited USize   := ⟨0⟩
 
 set_option bootstrap.gen_matcher_code false in

stage0/src/Init/LeanInit.lean

@@ -88,7 +88,7 @@ protected def beq : (@& Name) → (@& Name) → Bool
   | num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && Name.beq p₁ p₂
   | _,           _           => false
 
-instance : HasBeq Name := ⟨Name.beq⟩
+instance : BEq Name := ⟨Name.beq⟩
 
 def toStringWithSep (sep : String) : Name → String
   | anonymous         => "[anonymous]"
@@ -107,7 +107,7 @@ protected def append : Name → Name → Name
   | n, str p s _ => mkNameStr (Name.append n p) s
   | n, num p d _ => mkNameNum (Name.append n p) d
 
-instance : HasAppend Name := ⟨Name.append⟩
+instance : Append Name := ⟨Name.append⟩
 
 def capitalize : Name → Name
 | Name.str p s _ => mkNameStr p s.capitalize
@@ -844,43 +844,40 @@ def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
 end Syntax
 
 /-- Reflect a runtime datum back to surface syntax (best-effort). -/
-class HasQuote (α : Type) :=
-  (quote : α → Syntax)
-
-export HasQuote (quote)
-
 class Quote (α : Type) :=
   (quote : α → Syntax)
 
-instance : HasQuote Syntax := ⟨id⟩
-instance : HasQuote String := ⟨mkStxStrLit⟩
-instance : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
-instance : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
+export Quote (quote)
+
+instance : Quote Syntax := ⟨id⟩
+instance : Quote String := ⟨mkStxStrLit⟩
+instance : Quote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
+instance : Quote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
 
 private def quoteName : Name → Syntax
   | Name.anonymous => mkCIdent `Lean.Name.anonymous
   | Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s]
   | Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i]
 
-instance : HasQuote Name := ⟨quoteName⟩
+instance : Quote Name := ⟨quoteName⟩
 
-instance {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
+instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) :=
   ⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩
 
-private def quoteList {α : Type} [HasQuote α] : List α → Syntax
+private def quoteList {α : Type} [Quote α] : List α → Syntax
   | []      => mkCIdent `List.nil
   | (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs]
 
-instance {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
+instance {α : Type} [Quote α] : Quote (List α) := ⟨quoteList⟩
 
-instance {α : Type} [HasQuote α] : HasQuote (Array α) :=
+instance {α : Type} [Quote α] : Quote (Array α) :=
   ⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩
 
-private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
+private def quoteOption {α : Type} [Quote α] : Option α → Syntax
   | none     => mkIdent `Option.none
   | (some x) => mkCAppStx `Option.some #[quote x]
 
-instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
+instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) := ⟨quoteOption⟩
 
 end Lean
 

stage0/src/Init/System/IO.lean

@@ -35,7 +35,7 @@ def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
 instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
 instance (ε : Type) : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
 instance (ε : Type) : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
-instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩
+instance (α ε : Type) : OrElse (EIO ε α) := ⟨MonadExcept.orelse⟩
 instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
 
 open IO (Error) in
@@ -462,28 +462,22 @@ universe u
 namespace Lean
 
 /-- Typeclass used for presenting the output of an `#eval` command. -/
-class HasEval (α : Type u) :=
-  -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
-  -- so that `()` output is hidden in chained instances such as for some `m Unit`.
-  -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`)
-  (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit)
-
 class Eval (α : Type u) :=
   -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
   -- so that `()` output is hidden in chained instances such as for some `m Unit`.
   -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`)
   (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance {α : Type u} [Repr α] : HasEval α :=
+instance {α : Type u} [Repr α] : Eval α :=
   ⟨fun a _ => IO.println (repr (a ()))⟩
 
-instance : HasEval Unit :=
+instance : Eval Unit :=
   ⟨fun u hideUnit => if hideUnit then pure () else IO.println (repr (u ()))⟩
 
-instance {α : Type} [HasEval α] : HasEval (IO α) :=
-  ⟨fun x _ => do let a ← x (); HasEval.eval (fun _ => a)⟩
+instance {α : Type} [Eval α] : Eval (IO α) :=
+  ⟨fun x _ => do let a ← x (); Eval.eval (fun _ => a)⟩
 
-@[noinline, nospecialize] def runEval {α : Type u} [HasEval α] (a : Unit → α) : IO (String × Except IO.Error Unit) :=
-  IO.FS.withIsolatedStreams (HasEval.eval a false)
+@[noinline, nospecialize] def runEval {α : Type u} [Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit) :=
+  IO.FS.withIsolatedStreams (Eval.eval a false)
 
 end Lean

stage0/src/Init/WF.lean

@@ -38,10 +38,6 @@ end Acc
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop
   | intro (h : ∀ a, Acc r a) : WellFounded r
 
-class HasWellFounded (α : Sort u) : Type u :=
-  (r : α → α → Prop)
-  (wf : WellFounded r)
-
 class WellFoundedRelation (α : Sort u) : Type u :=
   (r : α → α → Prop)
   (wf : WellFounded r)
@@ -174,13 +170,13 @@ def measure {α : Sort u} : (α → Nat) → α → α → Prop :=
 def measureWf {α : Sort u} (f : α → Nat) : WellFounded (measure f) :=
   InvImage.wf f Nat.ltWf
 
-def sizeofMeasure (α : Sort u) [HasSizeof α] : α → α → Prop :=
-  measure sizeof
+def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop :=
+  measure sizeOf
 
-def sizeofMeasureWf (α : Sort u) [HasSizeof α] : WellFounded (sizeofMeasure α) :=
-  measureWf sizeof
+def sizeofMeasureWf (α : Sort u) [SizeOf α] : WellFounded (sizeofMeasure α) :=
+  measureWf sizeOf
 
-instance hasWellFoundedOfHasSizeof (α : Sort u) [HasSizeof α] : HasWellFounded α := {
+instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α := {
   r := sizeofMeasure α,
   wf := sizeofMeasureWf α
 }
@@ -237,7 +233,7 @@ def rprodWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Rprod ra
 
 end
 
-instance {α : Type u} {β : Type v} [s₁ : HasWellFounded α] [s₂ : HasWellFounded β] : HasWellFounded (α × β) := {
+instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) := {
   r  := Lex s₁.r s₂.r,
   wf := lexWf s₁.wf s₂.wf
 }
@@ -329,7 +325,7 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P
   RevLex.right _ _ h
 end
 
-instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (PSigma β) := {
+instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) := {
   r  := Lex s₁.r (fun a => (s₂ a).r),
   wf := lexWf s₁.wf (fun a => (s₂ a).wf)
 }

stage0/src/Lean/Attributes.lean

@@ -18,7 +18,7 @@ def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplica
   | AttributeApplicationTime.beforeElaboration, AttributeApplicationTime.beforeElaboration => true
   | _,                                          _                                          => false
 
-instance : HasBeq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩
+instance : BEq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩
 
 structure Attr.Context :=
   (currNamespace : Name)

stage0/src/Lean/Compiler/ConstFolding.lean

@@ -61,10 +61,10 @@ def foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (befor
   let info ← getInfoFromVal a₁
   pure $ mkUIntLit info (fn info beforeErasure n₁ n₂)
 
-def foldUIntAdd := foldBinUInt $ fun _ _ => HasAdd.add
-def foldUIntMul := foldBinUInt $ fun _ _ => HasMul.mul
-def foldUIntDiv := foldBinUInt $ fun _ _ => HasDiv.div
-def foldUIntMod := foldBinUInt $ fun _ _ => HasMod.mod
+def foldUIntAdd := foldBinUInt $ fun _ _ => Add.add
+def foldUIntMul := foldBinUInt $ fun _ _ => Mul.mul
+def foldUIntDiv := foldBinUInt $ fun _ _ => Div.div
+def foldUIntMod := foldBinUInt $ fun _ _ => Mod.mod
 def foldUIntSub := foldBinUInt $ fun info _ a b => (a + (info.size - b))
 
 def preUIntBinFoldFns : List (Name × BinFoldFn) :=
@@ -79,10 +79,10 @@ def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr :=
   let n₂   ← getNumLit a₂
   pure $ mkNatLit (fn n₁ n₂)
 
-def foldNatAdd (_ : Bool) := foldNatBinOp HasAdd.add
-def foldNatMul (_ : Bool) := foldNatBinOp HasMul.mul
-def foldNatDiv (_ : Bool) := foldNatBinOp HasDiv.div
-def foldNatMod (_ : Bool) := foldNatBinOp HasMod.mod
+def foldNatAdd (_ : Bool) := foldNatBinOp Add.add
+def foldNatMul (_ : Bool) := foldNatBinOp Mul.mul
+def foldNatDiv (_ : Bool) := foldNatBinOp Div.div
+def foldNatMod (_ : Bool) := foldNatBinOp Mod.mod
 
 -- TODO: add option for controlling the limit
 def natPowThreshold := 256

stage0/src/Lean/Compiler/ExternAttr.lean

@@ -122,7 +122,7 @@ def expandExternPattern (pattern : String) (args : List String) : String :=
   expandExternPatternAux args pattern.length pattern.mkIterator ""
 
 def mkSimpleFnCall (fn : String) (args : List String) : String :=
-  fn ++ "(" ++ ((args.intersperse ", ").foldl HasAppend.append "") ++ ")"
+  fn ++ "(" ++ ((args.intersperse ", ").foldl Append.append "") ++ ")"
 
 def ExternEntry.backend : ExternEntry → Name
   | ExternEntry.adhoc n      => n

stage0/src/Lean/Compiler/IR/Basic.lean

@@ -27,12 +27,12 @@ structure JoinPointId := (idx : Index)
 
 abbrev Index.lt (a b : Index) : Bool := a < b
 
-instance : HasBeq VarId := ⟨fun a b => a.idx == b.idx⟩
+instance : BEq VarId := ⟨fun a b => a.idx == b.idx⟩
 instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩
 instance : ToFormat VarId := ⟨fun a => toString a⟩
 instance : Hashable VarId := ⟨fun a => hash a.idx⟩
 
-instance : HasBeq JoinPointId := ⟨fun a b => a.idx == b.idx⟩
+instance : BEq JoinPointId := ⟨fun a b => a.idx == b.idx⟩
 instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
 instance : ToFormat JoinPointId := ⟨fun a => toString a⟩
 instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩
@@ -94,7 +94,7 @@ partial def beq : IRType → IRType → Bool
   | union n₁ tys₁,  union n₂ tys₂  => n₁ == n₂ && Array.isEqv tys₁ tys₂ beq
   | _,              _              => false
 
-instance : HasBeq IRType := ⟨beq⟩
+instance : BEq IRType := ⟨beq⟩
 
 def isScalar : IRType → Bool
   | float  => true
@@ -137,7 +137,7 @@ protected def Arg.beq : Arg → Arg → Bool
   | irrelevant, irrelevant => true
   | _,          _          => false
 
-instance : HasBeq Arg := ⟨Arg.beq⟩
+instance : BEq Arg := ⟨Arg.beq⟩
 instance : Inhabited Arg := ⟨Arg.irrelevant⟩
 
 @[export lean_ir_mk_var_arg] def mkVarArg (id : VarId) : Arg := Arg.var id
@@ -151,7 +151,7 @@ def LitVal.beq : LitVal → LitVal → Bool
   | str v₁, str v₂ => v₁ == v₂
   | _,      _      => false
 
-instance : HasBeq LitVal := ⟨LitVal.beq⟩
+instance : BEq LitVal := ⟨LitVal.beq⟩
 
 /- Constructor information.
 
@@ -175,7 +175,7 @@ def CtorInfo.beq : CtorInfo → CtorInfo → Bool
   | ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ =>
     n₁ == n₂ && cidx₁ == cidx₂ && size₁ == size₂ && usize₁ == usize₂ && ssize₁ == ssize₂
 
-instance : HasBeq CtorInfo := ⟨CtorInfo.beq⟩
+instance : BEq CtorInfo := ⟨CtorInfo.beq⟩
 
 def CtorInfo.isRef (info : CtorInfo) : Bool :=
   info.size > 0 || info.usize > 0 || info.ssize > 0
@@ -491,32 +491,29 @@ def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr :=
 
 abbrev IndexRenaming := RBMap Index Index Index.lt
 
-class HasAlphaEqv (α : Type) :=
-  (aeqv : IndexRenaming → α → α → Bool)
-
 class AlphaEqv (α : Type) :=
   (aeqv : IndexRenaming → α → α → Bool)
 
-export HasAlphaEqv (aeqv)
+export AlphaEqv (aeqv)
 
 def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool :=
   match ρ.find? v₁.idx with
   | some v => v == v₂.idx
   | none   => v₁ == v₂
 
-instance : HasAlphaEqv VarId := ⟨VarId.alphaEqv⟩
+instance : AlphaEqv VarId := ⟨VarId.alphaEqv⟩
 
 def Arg.alphaEqv (ρ : IndexRenaming) : Arg → Arg → Bool
   | Arg.var v₁,     Arg.var v₂     => aeqv ρ v₁ v₂
   | Arg.irrelevant, Arg.irrelevant => true
   | _,              _              => false
 
-instance : HasAlphaEqv Arg := ⟨Arg.alphaEqv⟩
+instance : AlphaEqv Arg := ⟨Arg.alphaEqv⟩
 
 def args.alphaEqv (ρ : IndexRenaming) (args₁ args₂ : Array Arg) : Bool :=
   Array.isEqv args₁ args₂ (fun a b => aeqv ρ a b)
 
-instance: HasAlphaEqv (Array Arg) := ⟨args.alphaEqv⟩
+instance: AlphaEqv (Array Arg) := ⟨args.alphaEqv⟩
 
 def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool
   | Expr.ctor i₁ ys₁,        Expr.ctor i₂ ys₂        => i₁ == i₂ && aeqv ρ ys₁ ys₂
@@ -535,7 +532,7 @@ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool
   | Expr.isTaggedPtr x₁,     Expr.isTaggedPtr x₂     => aeqv ρ x₁ x₂
   | _,                        _                      => false
 
-instance : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩
+instance : AlphaEqv Expr:= ⟨Expr.alphaEqv⟩
 
 def addVarRename (ρ : IndexRenaming) (x₁ x₂ : Nat) :=
   if x₁ == x₂ then ρ else ρ.insert x₁ x₂
@@ -575,7 +572,7 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
 def FnBody.beq (b₁ b₂ : FnBody) : Bool :=
   FnBody.alphaEqv ∅ b₁ b₂
 
-instance : HasBeq FnBody := ⟨FnBody.beq⟩
+instance : BEq FnBody := ⟨FnBody.beq⟩
 
 abbrev VarIdSet := RBTree VarId (fun x y => x.idx < y.idx)
 instance : Inhabited VarIdSet := ⟨{}⟩

stage0/src/Lean/Compiler/IR/Borrow.lean

@@ -16,7 +16,7 @@ abbrev Key := FunId × Index
 
 def beq : Key → Key → Bool
 | (f₁, x₁), (f₂, x₂) => f₁ == f₂ && x₁ == x₂
-instance : HasBeq Key := ⟨beq⟩
+instance : BEq Key := ⟨beq⟩
 
 def getHash : Key → USize
 | (f, x) => mixHash (hash f) (hash x)
@@ -43,7 +43,7 @@ def beq : Key → Key → Bool
 | Key.jp n₁ id₁, Key.jp n₂ id₂ => n₁ == n₂ && id₁ == id₂
 | _,         _                 => false
 
-instance : HasBeq Key := ⟨beq⟩
+instance : BEq Key := ⟨beq⟩
 
 def getHash : Key → USize
 | Key.decl n  => hash n

stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -30,7 +30,7 @@ protected partial def beq : Value → Value → Bool
   vs₂.all (fun v₂ => vs₁.any fun v₁ => Value.beq v₁ v₂)
 | _, _ => false
 
-instance : HasBeq Value := ⟨Value.beq⟩
+instance : BEq Value := ⟨Value.beq⟩
 
 partial def addChoice (merge : Value → Value → Value) : List Value → Value → List Value
 | [], v => [v]

stage0/src/Lean/Compiler/IR/FreeVars.lean

@@ -23,7 +23,7 @@ abbrev Collector := Index → Index
 @[inline] private def collectVar (x : VarId) : Collector := collect x.idx
 @[inline] private def collectJP (j : JoinPointId) : Collector := collect j.idx
 @[inline] private def seq (k₁ k₂ : Collector) : Collector := k₂ ∘ k₁
-instance : HasAndthen Collector := ⟨seq⟩
+instance : AndThen Collector := ⟨seq⟩
 
 private def collectArg : Arg → Collector
 | Arg.var x  => collectVar x
@@ -119,7 +119,7 @@ fun k bv fv => k (insertParams bv ys) fv
 @[inline] private def seq : Collector → Collector → Collector :=
 fun k₁ k₂ bv fv => k₂ bv (k₁ bv fv)
 
-instance : HasAndthen Collector := ⟨seq⟩
+instance : AndThen Collector := ⟨seq⟩
 
 private def collectArg : Arg → Collector
 | Arg.var x  => collectVar x

stage0/src/Lean/Compiler/InlineAttrs.lean

@@ -22,7 +22,7 @@ protected def beq : InlineAttributeKind → InlineAttributeKind → Bool
   | inlineIfReduce, inlineIfReduce => true
   | _, _ => false
 
-instance : HasBeq InlineAttributeKind := ⟨InlineAttributeKind.beq⟩
+instance : BEq InlineAttributeKind := ⟨InlineAttributeKind.beq⟩
 
 end InlineAttributeKind
 

stage0/src/Lean/Compiler/Specialize.lean

@@ -20,7 +20,7 @@ protected def beq : SpecializeAttributeKind → SpecializeAttributeKind → Bool
   | nospecialize, nospecialize => true
   | _, _ => false
 
-instance : HasBeq SpecializeAttributeKind := ⟨SpecializeAttributeKind.beq⟩
+instance : BEq SpecializeAttributeKind := ⟨SpecializeAttributeKind.beq⟩
 
 end SpecializeAttributeKind
 

stage0/src/Lean/Compiler/Util.lean

@@ -25,7 +25,7 @@ def Visitor := AtMostOnceData → AtMostOnceData
   | ⟨found, false⟩ => ⟨found, false⟩
   | other          => g other
 
-instance : HasAndthen Visitor := ⟨seq⟩
+instance : AndThen Visitor := ⟨seq⟩
 
 @[inline] def skip : Visitor := id
 

stage0/src/Lean/CoreM.lean

@@ -93,11 +93,11 @@ def mkFreshUserName {m} [MonadLiftT CoreM m] (n : Name) : m Name :=
   | Except.error (Exception.internal id) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
   | Except.ok a => pure a
 
-instance {α} [MetaHasEval α] : MetaHasEval (CoreM α) := {
+instance {α} [MetaEval α] : MetaEval (CoreM α) := {
   eval := fun env opts x _ => do
     let x : CoreM α := do try x finally printTraces
     let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env }
-    MetaHasEval.eval s.env opts a (hideUnit := true)
+    MetaEval.eval s.env opts a (hideUnit := true)
 }
 
 end Core

stage0/src/Lean/Data/Format.lean

@@ -14,7 +14,7 @@ inductive FlattenBehavior
   | fill
 
 namespace FlattenBehavior
-instance : HasBeq FlattenBehavior := ⟨fun b₁ b₂ =>
+instance : BEq FlattenBehavior := ⟨fun b₁ b₂ =>
   match b₁, b₂ with
   | allOrNone, allOrNone => true
   | fill,      fill      => true
@@ -45,12 +45,12 @@ protected def appendEx (a b : Format) : Format :=
 protected def groupEx : Format → Format :=
   group
 
-instance : HasAppend Format     := ⟨Format.append⟩
+instance : Append Format     := ⟨Format.append⟩
 instance : Coe String Format    := ⟨text⟩
 instance : Inhabited Format     := ⟨nil⟩
 
 def join (xs : List Format) : Format :=
-  xs.foldl HasAppend.append ""
+  xs.foldl Append.append ""
 
 def isNil : Format → Bool
   | nil => true

stage0/src/Lean/Data/Json/FromToJson.lean

@@ -10,63 +10,57 @@ namespace Lean
 
 universes u
 
-class HasFromJson (α : Type u) :=
-  (fromJson? : Json → Option α)
-
 class FromJson (α : Type u) :=
   (fromJson? : Json → Option α)
 
-export HasFromJson (fromJson?)
+export FromJson (fromJson?)
 
 class ToJson (α : Type u) :=
   (toJson : α → Json)
 
-class HasToJson (α : Type u) :=
-  (toJson : α → Json)
+export ToJson (toJson)
 
-export HasToJson (toJson)
+instance : FromJson Json := ⟨some⟩
+instance : ToJson Json := ⟨id⟩
 
-instance : HasFromJson Json := ⟨some⟩
-instance : HasToJson Json := ⟨id⟩
-
-instance : HasFromJson JsonNumber := ⟨Json.getNum?⟩
-instance : HasToJson JsonNumber := ⟨Json.num⟩
+instance : FromJson JsonNumber := ⟨Json.getNum?⟩
+instance : ToJson JsonNumber := ⟨Json.num⟩
 
 -- looks like id, but there are coercions happening
-instance : HasFromJson Bool := ⟨Json.getBool?⟩
-instance : HasToJson Bool := ⟨fun b => b⟩
-instance : HasFromJson Nat := ⟨Json.getNat?⟩
-instance : HasToJson Nat := ⟨fun n => n⟩
-instance : HasFromJson Int := ⟨Json.getInt?⟩
-instance : HasToJson Int := ⟨fun n => Json.num n⟩
-instance : HasFromJson String := ⟨Json.getStr?⟩
-instance : HasToJson String := ⟨fun s => s⟩
+instance : FromJson Bool := ⟨Json.getBool?⟩
+instance : ToJson Bool := ⟨fun b => b⟩
+instance : FromJson Nat := ⟨Json.getNat?⟩
+instance : ToJson Nat := ⟨fun n => n⟩
+instance : FromJson Int := ⟨Json.getInt?⟩
+instance : ToJson Int := ⟨fun n => Json.num n⟩
+instance : FromJson String := ⟨Json.getStr?⟩
+instance : ToJson String := ⟨fun s => s⟩
 
-instance {α : Type u} [HasFromJson α] : HasFromJson (Array α) := ⟨fun j =>
+instance {α : Type u} [FromJson α] : FromJson (Array α) := ⟨fun j =>
   match j with
   | Json.arr a => a.mapM fromJson?
   | _ => none⟩
 
-instance {α : Type u} [HasToJson α] : HasToJson (Array α) :=
+instance {α : Type u} [ToJson α] : ToJson (Array α) :=
   ⟨fun a => Json.arr (a.map toJson)⟩
 
 namespace Json
 
-instance : HasFromJson Structured := ⟨fun j =>
+instance : FromJson Structured := ⟨fun j =>
   match j with
   | arr a => Structured.arr a
   | obj o => Structured.obj o
   | _     => none⟩
 
-instance : HasToJson Structured := ⟨fun s =>
+instance : ToJson Structured := ⟨fun s =>
   match s with
   | Structured.arr a => arr a
   | Structured.obj o => obj o⟩
 
-def getObjValAs? (j : Json) (α : Type u) [HasFromJson α] (k : String) : Option α :=
+def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Option α :=
   (j.getObjVal? k).bind fromJson?
 
-def opt {α : Type u} [HasToJson α] (k : String) : Option α → List (String × Json)
+def opt {α : Type u} [ToJson α] (k : String) : Option α → List (String × Json)
   | some o => [⟨k, toJson o⟩]
   | none   => []
 

stage0/src/Lean/Data/JsonRpc.lean

@@ -38,7 +38,7 @@ inductive ErrorCode
   | requestCancelled
   | contentModified
 
-instance : HasFromJson ErrorCode := ⟨fun j =>
+instance : FromJson ErrorCode := ⟨fun j =>
   match j with
   | num (-32700 : Int) => ErrorCode.parseError
   | num (-32600 : Int) => ErrorCode.invalidRequest
@@ -53,7 +53,7 @@ instance : HasFromJson ErrorCode := ⟨fun j =>
   | num (-32801 : Int) => ErrorCode.contentModified
   | _  => none⟩
 
-instance : HasToJson ErrorCode := ⟨fun e =>
+instance : ToJson ErrorCode := ⟨fun e =>
   match e with
   | ErrorCode.parseError           => (-32700 : Int)
   | ErrorCode.invalidRequest       => (-32600 : Int)
@@ -85,19 +85,19 @@ structure Error := (id : RequestID) (code : JsonNumber) (message : String) (data
 instance : Coe String RequestID := ⟨RequestID.str⟩
 instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩
 
-instance : HasFromJson RequestID := ⟨fun j =>
+instance : FromJson RequestID := ⟨fun j =>
   match j with
   | str s => RequestID.str s
   | num n => RequestID.num n
   | _     => none⟩
 
-instance : HasToJson RequestID := ⟨fun rid =>
+instance : ToJson RequestID := ⟨fun rid =>
   match rid with
   | RequestID.str s => s
   | RequestID.num n => num n
   | RequestID.null  => null⟩
 
-instance : HasToJson Message := ⟨fun m =>
+instance : ToJson Message := ⟨fun m =>
   mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with
   | Message.request id method params? =>
     [ ⟨"id", toJson id⟩,
@@ -143,7 +143,7 @@ def aux4 (j : Json) : Option Message := do
 
 -- HACK: The implementation must be made up of several `auxN`s instead
 -- of one large block because of a bug in the compiler.
-instance : HasFromJson Message := ⟨fun j => do
+instance : FromJson Message := ⟨fun j => do
   let "2.0" ← j.getObjVal? "jsonrpc" | none
   aux1 j <|> aux2 j <|> aux3 j <|> aux4 j⟩
 
@@ -162,7 +162,7 @@ def readMessage (h : FS.Stream) (nBytes : Nat) : IO Message := do
   | some m => pure m
   | none   => throw (userError ("JSON '" ++ j.compress ++ "' did not have the format of a JSON-RPC message"))
 
-def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [HasFromJson α] : IO (Request α) := do
+def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
   let m ← h.readMessage nBytes
   match m with
   | Message.request id method params? =>
@@ -178,7 +178,7 @@ def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α :
       throw (userError ("expected method '" ++ expectedMethod ++ "', got method '" ++ method ++ "'"))
   | _ => throw (userError "expected request, got other type of message")
 
-def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [HasFromJson α] : IO α := do
+def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do
   let m ← h.readMessage nBytes
   match m with
   | Message.notification method params? =>
@@ -197,7 +197,7 @@ def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String)
 def writeMessage (h : FS.Stream) (m : Message) : IO Unit :=
   h.writeJson (toJson m)
 
-def writeResponse {α} [HasToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
+def writeResponse {α} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
   h.writeMessage (Message.response id (toJson r))
 
 end IO.FS.Stream

stage0/src/Lean/Data/KVMap.lean

@@ -33,7 +33,7 @@ def DataValue.sameCtor : DataValue → DataValue → Bool
 | DataValue.ofInt _,    DataValue.ofInt _    => true
 | _,                    _                    => false
 
-instance : HasBeq DataValue := ⟨DataValue.beq⟩
+instance : BEq DataValue := ⟨DataValue.beq⟩
 
 @[export lean_data_value_to_string]
 def DataValue.str : DataValue → String
@@ -143,7 +143,7 @@ def subset : KVMap → KVMap → Bool
 def eqv (m₁ m₂ : KVMap) : Bool :=
 subset m₁ m₂ && subset m₂ m₁
 
-instance : HasBeq KVMap := ⟨eqv⟩
+instance : BEq KVMap := ⟨eqv⟩
 
 class KVMapVal (α : Type) :=
 (defVal : α)

stage0/src/Lean/Data/LBool.lean

@@ -30,7 +30,7 @@ def beq : LBool → LBool → Bool
 | undef, undef => Bool.true
 | _,     _     => Bool.false
 
-instance : HasBeq LBool := ⟨beq⟩
+instance : BEq LBool := ⟨beq⟩
 
 def toString : LBool → String
 | true  => "true"

stage0/src/Lean/Data/LOption.lean

@@ -20,13 +20,13 @@ instance : Inhabited (LOption α) := ⟨none⟩
 instance [ToString α] : ToString (LOption α) :=
 ⟨fun o => match o with | none   => "none" | undef  => "undef" | (some a) => "(some " ++ toString a ++ ")"⟩
 
-def beq [HasBeq α] : LOption α → LOption α → Bool
+def beq [BEq α] : LOption α → LOption α → Bool
 | none,   none   => true
 | undef,  undef  => true
 | some a, some b => a == b
 | _,      _      => false
 
-instance [HasBeq α] : HasBeq (LOption α) := ⟨beq⟩
+instance [BEq α] : BEq (LOption α) := ⟨beq⟩
 
 end LOption
 end Lean

stage0/src/Lean/Data/Lsp/Basic.lean

@@ -27,12 +27,12 @@ structure Position := (line : Nat) (character : Nat)
 
 instance : Inhabited Position := ⟨⟨0, 0⟩⟩
 
-instance : HasFromJson Position := ⟨fun j => do
+instance : FromJson Position := ⟨fun j => do
   let line ← j.getObjValAs? Nat "line"
   let character ← j.getObjValAs? Nat "character"
   pure ⟨line, character⟩⟩
 
-instance : HasToJson Position := ⟨fun o =>
+instance : ToJson Position := ⟨fun o =>
   mkObj [
     ⟨"line", o.line⟩,
     ⟨"character", o.character⟩]⟩
@@ -42,24 +42,24 @@ instance : ToString Position := ⟨fun p =>
 
 structure Range := (start : Position) («end» : Position)
 
-instance : HasFromJson Range := ⟨fun j => do
+instance : FromJson Range := ⟨fun j => do
   let start ← j.getObjValAs? Position "start"
   let «end» ← j.getObjValAs? Position "end"
   pure ⟨start, «end»⟩⟩
 
-instance : HasToJson Range := ⟨fun o =>
+instance : ToJson Range := ⟨fun o =>
   mkObj [
     ⟨"start", toJson o.start⟩,
     ⟨"end", toJson o.«end»⟩]⟩
 
 structure Location := (uri : DocumentUri) (range : Range)
 
-instance : HasFromJson Location := ⟨fun j => do
+instance : FromJson Location := ⟨fun j => do
   let uri ← j.getObjValAs? DocumentUri "uri"
   let range ← j.getObjValAs? Range "range"
   pure ⟨uri, range⟩⟩
 
-instance : HasToJson Location := ⟨fun o =>
+instance : ToJson Location := ⟨fun o =>
   mkObj [
     ⟨"uri", toJson o.uri⟩,
     ⟨"range", toJson o.range⟩]⟩
@@ -70,14 +70,14 @@ structure LocationLink :=
   (targetRange : Range)
   (targetSelectionRange : Range)
 
-instance : HasFromJson LocationLink := ⟨fun j => do
+instance : FromJson LocationLink := ⟨fun j => do
   let originSelectionRange? := j.getObjValAs? Range "originSelectionRange"
   let targetUri ← j.getObjValAs? DocumentUri "targetUri"
   let targetRange ← j.getObjValAs? Range "targetRange"
   let targetSelectionRange ← j.getObjValAs? Range "targetSelectionRange"
   pure ⟨originSelectionRange?, targetUri, targetRange, targetSelectionRange⟩⟩
 
-instance : HasToJson LocationLink := ⟨fun o => mkObj $
+instance : ToJson LocationLink := ⟨fun o => mkObj $
   opt "originSelectionRange" o.originSelectionRange? ++ [
     ⟨"targetUri", toJson o.targetUri⟩,
     ⟨"targetRange", toJson o.targetRange⟩,
@@ -92,13 +92,13 @@ structure Command :=
   (command : String)
   (arguments? : Option (Array Json) := none)
 
-instance : HasFromJson Command := ⟨fun j => do
+instance : FromJson Command := ⟨fun j => do
   let title ← j.getObjValAs? String "title"
   let command ← j.getObjValAs? String "command"
   let arguments? := j.getObjValAs? (Array Json) "arguments"
   pure ⟨title, command, arguments?⟩⟩
 
-instance : HasToJson Command := ⟨fun o => mkObj $
+instance : ToJson Command := ⟨fun o => mkObj $
   opt "arguments" o.arguments? ++ [
     ⟨"title", o.title⟩,
     ⟨"command", o.command⟩]⟩
@@ -107,42 +107,42 @@ structure TextEdit :=
   (range : Range)
   (newText : String)
 
-instance : HasFromJson TextEdit := ⟨fun j => do
+instance : FromJson TextEdit := ⟨fun j => do
   let range ← j.getObjValAs? Range "range"
   let newText ← j.getObjValAs? String "newText"
   pure ⟨range, newText⟩⟩
 
-instance : HasToJson TextEdit := ⟨fun o =>
+instance : ToJson TextEdit := ⟨fun o =>
   mkObj [
     ⟨"range", toJson o.range⟩,
     ⟨"newText", o.newText⟩]⟩
 
 def TextEditBatch := Array TextEdit
 
-instance : HasFromJson TextEditBatch :=
+instance : FromJson TextEditBatch :=
   ⟨@fromJson? (Array TextEdit) _⟩
 
-instance  : HasToJson TextEditBatch :=
+instance  : ToJson TextEditBatch :=
   ⟨@toJson (Array TextEdit) _⟩
 
 structure TextDocumentIdentifier := (uri : DocumentUri)
 
-instance : HasFromJson TextDocumentIdentifier := ⟨fun j =>
+instance : FromJson TextDocumentIdentifier := ⟨fun j =>
   TextDocumentIdentifier.mk <$> j.getObjValAs? DocumentUri "uri"⟩
 
-instance : HasToJson TextDocumentIdentifier :=
+instance : ToJson TextDocumentIdentifier :=
   ⟨fun o => mkObj [⟨"uri", o.uri⟩]⟩
 
 structure VersionedTextDocumentIdentifier :=
   (uri : DocumentUri)
   (version? : Option Nat := none)
 
-instance : HasFromJson VersionedTextDocumentIdentifier := ⟨fun j => do
+instance : FromJson VersionedTextDocumentIdentifier := ⟨fun j => do
   let uri ← j.getObjValAs? DocumentUri "uri"
   let version? := j.getObjValAs? Nat "version"
   pure ⟨uri, version?⟩⟩
 
-instance : HasToJson VersionedTextDocumentIdentifier := ⟨fun o => mkObj $
+instance : ToJson VersionedTextDocumentIdentifier := ⟨fun o => mkObj $
   opt "version" o.version? ++
   [⟨"uri", o.uri⟩]⟩
 
@@ -150,12 +150,12 @@ structure TextDocumentEdit :=
   (textDocument : VersionedTextDocumentIdentifier)
   (edits : TextEditBatch)
 
-instance : HasFromJson TextDocumentEdit := ⟨fun j => do
+instance : FromJson TextDocumentEdit := ⟨fun j => do
   let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"
   let edits ← j.getObjValAs? TextEditBatch "edits"
   pure ⟨textDocument, edits⟩⟩
 
-instance : HasToJson TextDocumentEdit := ⟨fun o =>
+instance : ToJson TextDocumentEdit := ⟨fun o =>
   mkObj [
     ⟨"textDocument", toJson o.textDocument⟩,
     ⟨"edits", toJson o.edits⟩]⟩
@@ -171,14 +171,14 @@ structure TextDocumentItem :=
   (version : Nat)
   (text : String)
 
-instance : HasFromJson TextDocumentItem := ⟨fun j => do
+instance : FromJson TextDocumentItem := ⟨fun j => do
   let uri ← j.getObjValAs? DocumentUri "uri"
   let languageId ← j.getObjValAs? String "languageId"
   let version ← j.getObjValAs? Nat "version"
   let text ← j.getObjValAs? String "text"
   pure ⟨uri, languageId, version, text⟩⟩
 
-instance : HasToJson TextDocumentItem := ⟨fun o =>
+instance : ToJson TextDocumentItem := ⟨fun o =>
   mkObj [
     ⟨"uri", o.uri⟩,
     ⟨"languageId", o.languageId⟩,
@@ -189,12 +189,12 @@ structure TextDocumentPositionParams :=
   (textDocument : TextDocumentIdentifier)
   (position : Position)
 
-instance : HasFromJson TextDocumentPositionParams := ⟨fun j => do
+instance : FromJson TextDocumentPositionParams := ⟨fun j => do
   let textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument"
   let position ← j.getObjValAs? Position "position"
   pure ⟨textDocument, position⟩⟩
 
-instance : HasToJson TextDocumentPositionParams := ⟨fun o =>
+instance : ToJson TextDocumentPositionParams := ⟨fun o =>
   mkObj [
     ⟨"textDocument", toJson o.textDocument⟩,
     ⟨"position", toJson o.position⟩]⟩
@@ -204,62 +204,62 @@ structure DocumentFilter :=
   (scheme? : Option String := none)
   (pattern? : Option String := none)
 
-instance : HasFromJson DocumentFilter := ⟨fun j => do
+instance : FromJson DocumentFilter := ⟨fun j => do
   let language? := j.getObjValAs? String "language"
   let scheme? := j.getObjValAs? String "scheme"
   let pattern? := j.getObjValAs? String "pattern"
   pure ⟨language?, scheme?, pattern?⟩⟩
 
-instance : HasToJson DocumentFilter := ⟨fun o => mkObj $
+instance : ToJson DocumentFilter := ⟨fun o => mkObj $
   opt "language" o.language? ++
   opt "scheme" o.scheme? ++
   opt "pattern" o.pattern?⟩
 
 def DocumentSelector := Array DocumentFilter
 
-instance : HasFromJson DocumentSelector :=
+instance : FromJson DocumentSelector :=
   ⟨@fromJson? (Array DocumentFilter) _⟩
 
-instance : HasToJson DocumentSelector :=
+instance : ToJson DocumentSelector :=
   ⟨@toJson (Array DocumentFilter) _⟩
 
 structure StaticRegistrationOptions := (id? : Option String := none)
 
-instance : HasFromJson StaticRegistrationOptions :=
+instance : FromJson StaticRegistrationOptions :=
   ⟨fun j => some ⟨j.getObjValAs? String "id"⟩⟩
 
-instance : HasToJson StaticRegistrationOptions :=
+instance : ToJson StaticRegistrationOptions :=
   ⟨fun o => mkObj $ opt "id" o.id?⟩
 
 structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none)
 
-instance : HasFromJson TextDocumentRegistrationOptions :=
+instance : FromJson TextDocumentRegistrationOptions :=
   ⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩
 
-instance : HasToJson TextDocumentRegistrationOptions :=
+instance : ToJson TextDocumentRegistrationOptions :=
   ⟨fun o => mkObj $ opt "documentSelector" o.documentSelector?⟩
 
 inductive MarkupKind | plaintext | markdown
 
-instance : HasFromJson MarkupKind := ⟨fun j =>
+instance : FromJson MarkupKind := ⟨fun j =>
   match j with
   | str "plaintext" => some MarkupKind.plaintext
   | str "markdown"  => some MarkupKind.markdown
   | _               => none⟩
 
-instance : HasToJson MarkupKind := ⟨fun k =>
+instance : ToJson MarkupKind := ⟨fun k =>
   match k with
   | MarkupKind.plaintext => str "plaintext"
   | MarkupKind.markdown  => str "markdown"⟩
 
 structure MarkupContent := (kind : MarkupKind) (value : String)
 
-instance : HasFromJson MarkupContent := ⟨fun j => do
+instance : FromJson MarkupContent := ⟨fun j => do
   let kind ← j.getObjValAs? MarkupKind "kind"
   let value ← j.getObjValAs? String "value"
   pure ⟨kind, value⟩⟩
 
-instance : HasToJson MarkupContent := ⟨fun o =>
+instance : ToJson MarkupContent := ⟨fun o =>
   mkObj [
     ⟨"kind", toJson o.kind⟩,
     ⟨"value", o.value⟩]⟩

stage0/src/Lean/Data/Lsp/Capabilities.lean

@@ -19,7 +19,7 @@ open Json
 -- TODO: right now we ignore the client's capabilities
 inductive ClientCapabilities | mk
 
-instance : HasFromJson ClientCapabilities :=
+instance : FromJson ClientCapabilities :=
   ⟨fun j => ClientCapabilities.mk⟩
 
 -- TODO largely unimplemented
@@ -27,7 +27,7 @@ structure ServerCapabilities :=
   (textDocumentSync? : Option TextDocumentSyncOptions := none)
   (hoverProvider : Bool := false)
 
-instance : HasToJson ServerCapabilities := ⟨fun o => mkObj $
+instance : ToJson ServerCapabilities := ⟨fun o => mkObj $
   opt "textDocumentSync" o.textDocumentSync? ++
   [⟨"hoverProvider", o.hoverProvider⟩]⟩
 

stage0/src/Lean/Data/Lsp/Communication.lean

@@ -51,11 +51,11 @@ def readLspMessage (h : FS.Stream) : IO Message := do
   let nBytes ← readLspHeader h
   h.readMessage nBytes
 
-def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [HasFromJson α] : IO (Request α) := do
+def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
   let nBytes ← readLspHeader h
   h.readRequestAs nBytes expectedMethod α
 
-def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [HasFromJson α] : IO α := do
+def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do
   let nBytes ← readLspHeader h
   h.readNotificationAs nBytes expectedMethod α
 
@@ -67,10 +67,10 @@ def writeLspMessage (h : FS.Stream) (m : Message) : IO Unit := do
   h.putStr (header ++ j)
   h.flush
 
-def writeLspResponse {α : Type} [HasToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
+def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
   writeLspMessage h (Message.response id (toJson r))
 
-def writeLspNotification {α : Type} [HasToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
+def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
   match toJson r with
   | Json.obj o => writeLspMessage h (Message.notification method o)
   | Json.arr a => writeLspMessage h (Message.notification method a)

stage0/src/Lean/Data/Lsp/Diagnostics.lean

@@ -21,7 +21,7 @@ open Json
 inductive DiagnosticSeverity
   | error | warning | information | hint
 
-instance : HasFromJson DiagnosticSeverity := ⟨fun j =>
+instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
   | some 1 => DiagnosticSeverity.error
   | some 2 => DiagnosticSeverity.warning
@@ -29,7 +29,7 @@ instance : HasFromJson DiagnosticSeverity := ⟨fun j =>
   | some 4 => DiagnosticSeverity.hint
   | _      => none⟩
 
-instance : HasToJson DiagnosticSeverity := ⟨fun o =>
+instance : ToJson DiagnosticSeverity := ⟨fun o =>
   match o with
   | DiagnosticSeverity.error       => 1
   | DiagnosticSeverity.warning     => 2
@@ -40,13 +40,13 @@ inductive DiagnosticCode
   | int (i : Int)
   | string (s : String)
 
-instance : HasFromJson DiagnosticCode := ⟨fun j =>
+instance : FromJson DiagnosticCode := ⟨fun j =>
   match j with
   | num (i : Int) => DiagnosticCode.int i
   | str s         => DiagnosticCode.string s
   | _             => none⟩
 
-instance : HasToJson DiagnosticCode := ⟨fun o =>
+instance : ToJson DiagnosticCode := ⟨fun o =>
   match o with
   | DiagnosticCode.int i    => i
   | DiagnosticCode.string s => s⟩
@@ -55,13 +55,13 @@ inductive DiagnosticTag
   | unnecessary
   | deprecated
 
-instance : HasFromJson DiagnosticTag := ⟨fun j =>
+instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
   | some 1 => DiagnosticTag.unnecessary
   | some 2 => DiagnosticTag.deprecated
   | _      => none⟩
 
-instance : HasToJson DiagnosticTag := ⟨fun o =>
+instance : ToJson DiagnosticTag := ⟨fun o =>
   match o with
   | DiagnosticTag.unnecessary => (1 : Nat)
   | DiagnosticTag.deprecated  => (2 : Nat)⟩
@@ -70,12 +70,12 @@ structure DiagnosticRelatedInformation :=
   (location : Location)
   (message : String)
 
-instance : HasFromJson DiagnosticRelatedInformation := ⟨fun j => do
+instance : FromJson DiagnosticRelatedInformation := ⟨fun j => do
   let location ← j.getObjValAs? Location "location"
   let message ← j.getObjValAs? String "message"
   pure ⟨location, message⟩⟩
 
-instance : HasToJson DiagnosticRelatedInformation := ⟨fun o =>
+instance : ToJson DiagnosticRelatedInformation := ⟨fun o =>
   mkObj [
     ⟨"location", toJson o.location⟩,
     ⟨"message", o.message⟩]⟩
@@ -89,7 +89,7 @@ structure Diagnostic :=
   (tags? : Option (Array DiagnosticTag) := none)
   (relatedInformation? : Option (Array DiagnosticRelatedInformation) := none)
 
-instance : HasFromJson Diagnostic := ⟨fun j => do
+instance : FromJson Diagnostic := ⟨fun j => do
   let range ← j.getObjValAs? Range "range"
   let severity? := j.getObjValAs? DiagnosticSeverity "severity"
   let code? := j.getObjValAs? DiagnosticCode "code"
@@ -99,7 +99,7 @@ instance : HasFromJson Diagnostic := ⟨fun j => do
   let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation"
   pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
 
-instance : HasToJson Diagnostic := ⟨fun o => mkObj $
+instance : ToJson Diagnostic := ⟨fun o => mkObj $
   opt "severity" o.severity? ++
   opt "code" o.code? ++
   opt "source" o.source? ++
@@ -113,13 +113,13 @@ structure PublishDiagnosticsParams :=
   (version? : Option Int := none)
   (diagnostics: Array Diagnostic)
 
-instance : HasFromJson PublishDiagnosticsParams := ⟨fun j => do
+instance : FromJson PublishDiagnosticsParams := ⟨fun j => do
   let uri ← j.getObjValAs? DocumentUri "uri"
   let version? := j.getObjValAs? Int "version"
   let diagnostics ← j.getObjValAs? (Array Diagnostic) "diagnostics"
   pure ⟨uri, version?, diagnostics⟩⟩
 
-instance : HasToJson PublishDiagnosticsParams := ⟨fun o => mkObj $
+instance : ToJson PublishDiagnosticsParams := ⟨fun o => mkObj $
   opt "version" o.version? ++ [
     ⟨"uri", toJson o.uri⟩,
     ⟨"diagnostics", toJson o.diagnostics⟩]⟩

stage0/src/Lean/Data/Lsp/Hover.lean

@@ -20,22 +20,22 @@ structure Hover :=
   (contents : MarkupContent)
   (range? : Option Range := none)
 
-instance : HasFromJson Hover := ⟨fun j => do
+instance : FromJson Hover := ⟨fun j => do
   let contents ← j.getObjValAs? MarkupContent "contents"
   let range? := j.getObjValAs? Range "range"
   pure ⟨contents, range?⟩⟩
 
-instance : HasToJson Hover := ⟨fun o => mkObj $
+instance : ToJson Hover := ⟨fun o => mkObj $
   ⟨"contents", toJson o.contents⟩ ::
   opt "range" o.range?⟩
 
 structure HoverParams extends TextDocumentPositionParams
 
-instance : HasFromJson HoverParams := ⟨fun j => do
+instance : FromJson HoverParams := ⟨fun j => do
   let tdpp ← @fromJson? TextDocumentPositionParams _ j
   pure ⟨tdpp⟩⟩
 
-instance : HasToJson HoverParams :=
+instance : ToJson HoverParams :=
   ⟨fun o => toJson o.toTextDocumentPositionParams⟩
 
 end Lsp

stage0/src/Lean/Data/Lsp/InitShutdown.lean

@@ -20,7 +20,7 @@ structure ClientInfo :=
   (name : String)
   (version? : Option String := none)
 
-instance : HasFromJson ClientInfo := ⟨fun j => do
+instance : FromJson ClientInfo := ⟨fun j => do
   let name ← j.getObjValAs? String "name"
   let version? := j.getObjValAs? String "version"
   pure ⟨name, version?⟩⟩
@@ -30,7 +30,7 @@ inductive Trace
   | messages
   | verbose
 
-instance : HasFromJson Trace := ⟨fun j =>
+instance : FromJson Trace := ⟨fun j =>
   match j.getStr? with
   | some "off"      => Trace.off
   | some "messages" => Trace.messages
@@ -49,7 +49,7 @@ structure InitializeParams :=
   (trace : Trace := Trace.off)
   (workspaceFolders? : Option (Array WorkspaceFolder) := none)
 
-instance : HasFromJson InitializeParams := ⟨fun j => do
+instance : FromJson InitializeParams := ⟨fun j => do
   /- Many of these params can be null instead of not present.
   For ease of implementation, we're liberal:
   missing params, wrong json types and null all map to none,
@@ -68,14 +68,14 @@ instance : HasFromJson InitializeParams := ⟨fun j => do
 
 inductive InitializedParams | mk
 
-instance : HasFromJson InitializedParams :=
+instance : FromJson InitializedParams :=
   ⟨fun j => InitializedParams.mk⟩
 
 structure ServerInfo :=
   (name : String)
   (version? : Option String := none)
 
-instance : HasToJson ServerInfo := ⟨fun o => mkObj $
+instance : ToJson ServerInfo := ⟨fun o => mkObj $
   ⟨"name", o.name⟩ ::
   opt "version" o.version?⟩
 
@@ -83,7 +83,7 @@ structure InitializeResult :=
   (capabilities : ServerCapabilities)
   (serverInfo? : Option ServerInfo := none)
 
-instance : HasToJson InitializeResult := ⟨fun o =>
+instance : ToJson InitializeResult := ⟨fun o =>
   mkObj $
      ⟨"capabilities", toJson o.capabilities⟩ ::
      opt "serverInfo" o.serverInfo?⟩

stage0/src/Lean/Data/Lsp/TextSync.lean

@@ -19,14 +19,14 @@ inductive TextDocumentSyncKind
   | full
   | incremental
 
-instance : HasFromJson TextDocumentSyncKind := ⟨fun j =>
+instance : FromJson TextDocumentSyncKind := ⟨fun j =>
   match j.getNat? with
   | some 0 => TextDocumentSyncKind.none
   | some 1 => TextDocumentSyncKind.full
   | some 2 => TextDocumentSyncKind.incremental
   | _      => none⟩
 
-instance : HasToJson TextDocumentSyncKind := ⟨fun o =>
+instance : ToJson TextDocumentSyncKind := ⟨fun o =>
   match o with
   | TextDocumentSyncKind.none        => 0
   | TextDocumentSyncKind.full        => 1
@@ -35,17 +35,17 @@ instance : HasToJson TextDocumentSyncKind := ⟨fun o =>
 structure DidOpenTextDocumentParams :=
   (textDocument : TextDocumentItem)
 
-instance : HasFromJson DidOpenTextDocumentParams := ⟨fun j =>
+instance : FromJson DidOpenTextDocumentParams := ⟨fun j =>
   DidOpenTextDocumentParams.mk <$> j.getObjValAs? TextDocumentItem "textDocument"⟩
 
-instance : HasToJson DidOpenTextDocumentParams := ⟨fun o =>
+instance : ToJson DidOpenTextDocumentParams := ⟨fun o =>
   mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩
 
 structure TextDocumentChangeRegistrationOptions :=
   (documentSelector? : Option DocumentSelector := none)
   (syncKind : TextDocumentSyncKind)
 
-instance : HasFromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do
+instance : FromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do
   let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector";
   let syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind";
   pure ⟨documentSelector?, syncKind⟩⟩
@@ -55,7 +55,7 @@ inductive TextDocumentContentChangeEvent
   | rangeChange (range : Range) (text : String)
   | fullChange (text : String)
 
-instance : HasFromJson TextDocumentContentChangeEvent := ⟨fun j =>
+instance : FromJson TextDocumentContentChangeEvent := ⟨fun j =>
   (do
     let range ← j.getObjValAs? Range "range"
     let text ← j.getObjValAs? String "text"
@@ -66,7 +66,7 @@ structure DidChangeTextDocumentParams :=
   (textDocument : VersionedTextDocumentIdentifier)
   (contentChanges : Array TextDocumentContentChangeEvent)
 
-instance : HasFromJson DidChangeTextDocumentParams := ⟨fun j => do
+instance : FromJson DidChangeTextDocumentParams := ⟨fun j => do
   let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"
   let contentChanges ← j.getObjValAs? (Array TextDocumentContentChangeEvent) "contentChanges"
   pure ⟨textDocument, contentChanges⟩⟩
@@ -77,12 +77,12 @@ instance : HasFromJson DidChangeTextDocumentParams := ⟨fun j => do
 
 structure SaveOptions := (includeText : Bool)
 
-instance : HasToJson SaveOptions := ⟨fun o =>
+instance : ToJson SaveOptions := ⟨fun o =>
   mkObj $ [⟨"includeText", o.includeText⟩]⟩
 
 structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier)
 
-instance : HasFromJson DidCloseTextDocumentParams := ⟨fun j =>
+instance : FromJson DidCloseTextDocumentParams := ⟨fun j =>
   DidCloseTextDocumentParams.mk <$> j.getObjValAs? TextDocumentIdentifier "textDocument"⟩
 
 -- TODO: TextDocumentSyncClientCapabilities
@@ -95,7 +95,7 @@ structure TextDocumentSyncOptions :=
   (willSaveWaitUntil : Bool)
   (save? : Option SaveOptions := none)
 
-instance : HasToJson TextDocumentSyncOptions := ⟨fun o =>
+instance : ToJson TextDocumentSyncOptions := ⟨fun o =>
   mkObj $
     opt "save" o.save? ++ [
       ⟨"openClose", toJson o.openClose⟩,

stage0/src/Lean/Data/Lsp/Workspace.lean

@@ -16,12 +16,12 @@ structure WorkspaceFolder :=
   (uri : DocumentUri)
   (name : String)
 
-instance : HasFromJson WorkspaceFolder := ⟨fun j => do
+instance : FromJson WorkspaceFolder := ⟨fun j => do
   let uri ← j.getObjValAs? DocumentUri "uri"
   let name ← j.getObjValAs? String "name"
   pure ⟨uri, name⟩⟩
 
-instance : HasToJson WorkspaceFolder := ⟨fun o =>
+instance : ToJson WorkspaceFolder := ⟨fun o =>
   mkObj [
     ⟨"uri", toJson o.uri⟩,
     ⟨"name", toJson o.name⟩]⟩

stage0/src/Lean/Data/Name.lean

@@ -93,10 +93,10 @@ else if n₁.hash > n₂.hash then false
 else quickLtAux n₁ n₂
 
 /- Alternative HasLt instance. -/
-@[inline] protected def hasLtQuick : HasLess Name :=
+@[inline] protected def hasLtQuick : Less Name :=
 ⟨fun a b => Name.quickLt a b = true⟩
 
-@[inline] instance : DecidableRel (@HasLess.Less Name Name.hasLtQuick) :=
+@[inline] instance : DecidableRel (@Less.Less Name Name.hasLtQuick) :=
 inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true))
 
 /- The frontend does not allow user declarations to start with `_` in any of its parts.
@@ -135,7 +135,7 @@ def NameMap (α : Type) := Std.RBMap Name α Name.quickLt
 namespace NameMap
 variable {α : Type}
 
-instance (α : Type) : HasEmptyc (NameMap α) := ⟨mkNameMap α⟩
+instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩
 
 instance (α : Type) : Inhabited (NameMap α) := ⟨{}⟩
 
@@ -151,7 +151,7 @@ def NameSet := RBTree Name Name.quickLt
 
 namespace NameSet
 def empty : NameSet := mkRBTree Name Name.quickLt
-instance : HasEmptyc NameSet := ⟨empty⟩
+instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨{}⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n
 def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n
@@ -162,7 +162,7 @@ def NameHashSet := Std.HashSet Name
 
 namespace NameHashSet
 @[inline] def empty : NameHashSet := Std.HashSet.empty
-instance : HasEmptyc NameHashSet := ⟨empty⟩
+instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n

stage0/src/Lean/Data/Occurrences.lean

@@ -30,7 +30,7 @@ def beq : Occurrences → Occurrences → Bool
 | neg is₁, neg is₂ => is₁ == is₂
 | _,       _       => false
 
-instance : HasBeq Occurrences := ⟨beq⟩
+instance : BEq Occurrences := ⟨beq⟩
 
 end Occurrences
 

stage0/src/Lean/Data/SMap.lean

@@ -27,13 +27,13 @@ open Std (HashMap PHashMap)
      that an entry was "removed" from the hashtable.
    - We do not need additional bookkeeping for extracting the local entries.
 -/
-structure SMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] :=
+structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
 (stage₁ : Bool         := true)
 (map₁   : HashMap α β  := {})
 (map₂   : PHashMap α β := {})
 
 namespace SMap
-variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α]
+variables {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
 instance : Inhabited (SMap α β) := ⟨{}⟩
 def empty : SMap α β := {}

stage0/src/Lean/Data/Trie.lean

@@ -21,7 +21,7 @@ variables {α : Type}
 def empty : Trie α :=
 ⟨none, RBNode.leaf⟩
 
-instance : HasEmptyc (Trie α) :=
+instance : EmptyCollection (Trie α) :=
 ⟨empty⟩
 
 instance : Inhabited (Trie α) :=

stage0/src/Lean/Delaborator.lean

@@ -48,7 +48,7 @@ protected partial def quote : Level → Syntax
   -- HACK: approximation
   | mvar  n _    => Unhygienic.run `(level|_)
 
-instance : HasQuote Level := ⟨Level.quote⟩
+instance : Quote Level := ⟨Level.quote⟩
 end Level
 
 def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
@@ -104,7 +104,7 @@ instance : Alternative DelabM := {
   failure := Delaborator.failure
 }
 -- HACK: necessary since it would otherwise prefer the instance from MonadExcept
-instance {α} : HasOrelse (DelabM α) := ⟨Delaborator.orelse⟩
+instance {α} : OrElse (DelabM α) := ⟨Delaborator.orelse⟩
 
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
@@ -507,7 +507,7 @@ def delabLit : Delab := do
   | Literal.strVal s => pure $ quote s
 
 -- `ofNat 0` ~> `0`
-@[builtinDelab app.HasOfNat.ofNat]
+@[builtinDelab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
   let e@(Expr.app _ (Expr.lit (Literal.natVal n) _) _) ← getExpr | failure
   pure $ quote n
@@ -627,24 +627,24 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
 @[builtinDelab app.Prod] def delabProd : Delab := delabInfixOp fun _ x y => `($x × $y)
 @[builtinDelab app.Function.comp] def delabFComp : Delab := delabInfixOp fun _ x y => `($x ∘ $y)
 
-@[builtinDelab app.HasAdd.add] def delabAdd : Delab := delabInfixOp fun _ x y => `($x + $y)
-@[builtinDelab app.HasSub.sub] def delabSub : Delab := delabInfixOp fun _ x y => `($x - $y)
-@[builtinDelab app.HasMul.mul] def delabMul : Delab := delabInfixOp fun _ x y => `($x * $y)
-@[builtinDelab app.HasDiv.div] def delabDiv : Delab := delabInfixOp fun _ x y => `($x / $y)
-@[builtinDelab app.HasMod.mod] def delabMod : Delab := delabInfixOp fun _ x y => `($x % $y)
-@[builtinDelab app.HasModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y)
-@[builtinDelab app.HasPow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y)
+@[builtinDelab app.Add.add] def delabAdd : Delab := delabInfixOp fun _ x y => `($x + $y)
+@[builtinDelab app.Sub.sub] def delabSub : Delab := delabInfixOp fun _ x y => `($x - $y)
+@[builtinDelab app.Mul.mul] def delabMul : Delab := delabInfixOp fun _ x y => `($x * $y)
+@[builtinDelab app.Div.div] def delabDiv : Delab := delabInfixOp fun _ x y => `($x / $y)
+@[builtinDelab app.Mod.mod] def delabMod : Delab := delabInfixOp fun _ x y => `($x % $y)
+@[builtinDelab app.ModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y)
+@[builtinDelab app.Pow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y)
 
-@[builtinDelab app.HasLessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
+@[builtinDelab app.LessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
 @[builtinDelab app.GreaterEq] def delabGE : Delab := delabInfixOp fun b x y => cond b `($x ≥ $y) `($x >= $y)
-@[builtinDelab app.HasLess.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
+@[builtinDelab app.Less.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
 @[builtinDelab app.Greater] def delabGT : Delab := delabInfixOp fun _ x y => `($x > $y)
 @[builtinDelab app.Eq] def delabEq : Delab := delabInfixOp fun _ x y => `($x = $y)
 @[builtinDelab app.Ne] def delabNe : Delab := delabInfixOp fun _ x y => `($x ≠ $y)
-@[builtinDelab app.HasBeq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y)
+@[builtinDelab app.BEq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y)
 @[builtinDelab app.bne] def delabBNe : Delab := delabInfixOp fun _ x y => `($x != $y)
 @[builtinDelab app.HEq] def delabHEq : Delab := delabInfixOp fun b x y => cond b `($x ≅ $y) `($x ~= $y)
-@[builtinDelab app.HasEquiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
+@[builtinDelab app.Equiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
 
 @[builtinDelab app.And] def delabAnd : Delab := delabInfixOp fun b x y => cond b `($x ∧ $y) `($x /\ $y)
 @[builtinDelab app.Or] def delabOr : Delab := delabInfixOp fun b x y => cond b `($x ∨ $y) `($x || $y)
@@ -653,20 +653,20 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
 @[builtinDelab app.and] def delabBAnd : Delab := delabInfixOp fun _ x y => `($x && $y)
 @[builtinDelab app.or] def delabBOr : Delab := delabInfixOp fun _ x y => `($x || $y)
 
-@[builtinDelab app.HasAppend.append] def delabAppend : Delab := delabInfixOp fun _ x y => `($x ++ $y)
+@[builtinDelab app.Append.append] def delabAppend : Delab := delabInfixOp fun _ x y => `($x ++ $y)
 @[builtinDelab app.List.cons] def delabCons : Delab := delabInfixOp fun _ x y => `($x :: $y)
 
-@[builtinDelab app.HasAndthen.andthen] def delabAndThen : Delab := delabInfixOp fun _ x y => `($x >> $y)
-@[builtinDelab app.HasBind.bind] def delabBind : Delab := delabInfixOp fun _ x y => `($x >>= $y)
+@[builtinDelab app.AndThen.andthen] def delabAndThen : Delab := delabInfixOp fun _ x y => `($x >> $y)
+@[builtinDelab app.Bind.bind] def delabBind : Delab := delabInfixOp fun _ x y => `($x >>= $y)
 
-@[builtinDelab app.HasSeq.seq] def delabseq : Delab := delabInfixOp fun _ x y => `($x <*> $y)
-@[builtinDelab app.HasSeqLeft.seqLeft] def delabseqLeft : Delab := delabInfixOp fun _ x y => `($x <* $y)
-@[builtinDelab app.HasSeqRight.seqRight] def delabseqRight : Delab := delabInfixOp fun _ x y => `($x *> $y)
+@[builtinDelab app.Seq.seq] def delabseq : Delab := delabInfixOp fun _ x y => `($x <*> $y)
+@[builtinDelab app.SeqLeft.seqLeft] def delabseqLeft : Delab := delabInfixOp fun _ x y => `($x <* $y)
+@[builtinDelab app.SeqRight.seqRight] def delabseqRight : Delab := delabInfixOp fun _ x y => `($x *> $y)
 
 @[builtinDelab app.Functor.map] def delabMap : Delab := delabInfixOp fun _ x y => `($x <$> $y)
 @[builtinDelab app.Functor.mapRev] def delabMapRev : Delab := delabInfixOp fun _ x y => `($x <&> $y)
 
-@[builtinDelab app.HasOrelse.orelse] def delabOrElse : Delab := delabInfixOp fun _ x y => `($x <|> $y)
+@[builtinDelab app.OrElse.orelse] def delabOrElse : Delab := delabInfixOp fun _ x y => `($x <|> $y)
 @[builtinDelab app.orM] def delabOrM : Delab := delabInfixOp fun _ x y => `($x <||> $y)
 @[builtinDelab app.andM] def delabAndM : Delab := delabInfixOp fun _ x y => `($x <&&> $y)
 

stage0/src/Lean/Elab/Tactic/Basic.lean

@@ -59,7 +59,7 @@ instance : MonadExcept Exception TacticM := {
   tryCatch := Tactic.tryCatch
 }
 
-instance {α} : HasOrelse (TacticM α) := ⟨Tactic.orelse⟩
+instance {α} : OrElse (TacticM α) := ⟨Tactic.orelse⟩
 
 structure SavedState :=
   (core   : Core.State)

stage0/src/Lean/Elab/Term.lean

@@ -1276,13 +1276,13 @@ private def mkSomeContext : Context := {
   let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta
   pure (a, sCore, sMeta, s)
 
-instance {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
+instance {α} [MetaEval α] : MetaEval (TermElabM α) :=
   ⟨fun env opts x _ =>
     let x : TermElabM α := do
       try x finally
         let s ← get
         liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println
-    MetaHasEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩
+    MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩
 
 end Term
 

stage0/src/Lean/Eval.lean

@@ -9,16 +9,16 @@ namespace Lean
 
 universe u
 
-/-- `HasEval` extension that gives access to the current environment & options.
-    The basic `HasEval` class is in the prelude and should not depend on these
+/-- `Eval` extension that gives access to the current environment & options.
+    The basic `Eval` class is in the prelude and should not depend on these
     types. -/
-class MetaHasEval (α : Type u) :=
+class MetaEval (α : Type u) :=
 (eval : Environment → Options → α → (hideUnit : Bool) → IO Environment)
 
-instance {α : Type u} [HasEval α] : MetaHasEval α :=
-⟨fun env opts a hideUnit => do HasEval.eval (fun _ => a) hideUnit; pure env⟩
+instance {α : Type u} [Eval α] : MetaEval α :=
+⟨fun env opts a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩
 
-def runMetaEval {α : Type u} [MetaHasEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
-IO.FS.withIsolatedStreams (MetaHasEval.eval env opts a false)
+def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
+IO.FS.withIsolatedStreams (MetaEval.eval env opts a false)
 
 end Lean

stage0/src/Lean/Expr.lean

@@ -25,7 +25,7 @@ def Literal.beq : Literal → Literal → Bool
   | Literal.strVal v₁, Literal.strVal v₂ => v₁ == v₂
   | _,                 _                 => false
 
-instance : HasBeq Literal := ⟨Literal.beq⟩
+instance : BEq Literal := ⟨Literal.beq⟩
 
 def Literal.lt : Literal → Literal → Bool
   | Literal.natVal _,  Literal.strVal _  => true
@@ -33,7 +33,7 @@ def Literal.lt : Literal → Literal → Bool
   | Literal.strVal v₁, Literal.strVal v₂ => v₁ < v₂
   | _,                 _                 => false
 
-instance : HasLess Literal := ⟨fun a b => a.lt b⟩
+instance : Less Literal := ⟨fun a b => a.lt b⟩
 
 instance (a b : Literal) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.lt b))
@@ -74,7 +74,7 @@ protected def BinderInfo.beq : BinderInfo → BinderInfo → Bool
   | BinderInfo.auxDecl,        BinderInfo.auxDecl        => true
   | _,                         _                         => false
 
-instance : HasBeq BinderInfo := ⟨BinderInfo.beq⟩
+instance : BEq BinderInfo := ⟨BinderInfo.beq⟩
 
 abbrev MData := KVMap
 abbrev MData.empty : MData := {}
@@ -97,7 +97,7 @@ instance: Inhabited Expr.Data :=
 def Expr.Data.hash (c : Expr.Data) : USize :=
   c.toUInt32.toUSize
 
-instance : HasBeq Expr.Data :=
+instance : BEq Expr.Data :=
   ⟨fun (a b : UInt64) => a == b⟩
 
 def Expr.Data.looseBVarRange (c : Expr.Data) : UInt32 :=
@@ -388,7 +388,7 @@ constant lt (a : @& Expr) (b : @& Expr) : Bool
 @[extern "lean_expr_eqv"]
 constant eqv (a : @& Expr) (b : @& Expr) : Bool
 
-instance : HasBeq Expr := ⟨Expr.eqv⟩
+instance : BEq Expr := ⟨Expr.eqv⟩
 
 /- Return true iff `a` and `b` are equal.
    Binder names and annotations are taking into account. -/
@@ -735,7 +735,7 @@ protected def hash : ExprStructEq → USize
   | ⟨e⟩ => e.hash
 
 instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩
-instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩
+instance : BEq ExprStructEq := ⟨ExprStructEq.beq⟩
 instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
 instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩
 instance : Repr ExprStructEq := ⟨fun e => repr e.val⟩

stage0/src/Lean/HeadIndex.lean

@@ -44,7 +44,7 @@ protected def HeadIndex.beq : HeadIndex → HeadIndex → Bool
 | forallE,    forallE    => true
 | _,          _          => false
 
-instance : HasBeq HeadIndex := ⟨HeadIndex.beq⟩
+instance : BEq HeadIndex := ⟨HeadIndex.beq⟩
 
 end HeadIndex
 

stage0/src/Lean/InternalExceptionId.lean

@@ -9,7 +9,7 @@ structure InternalExceptionId :=
   (idx : Nat := 0)
 
 instance : Inhabited InternalExceptionId := ⟨{}⟩
-instance : HasBeq InternalExceptionId :=
+instance : BEq InternalExceptionId :=
   ⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
 
 builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[]

stage0/src/Lean/Level.lean

@@ -29,7 +29,7 @@ instance : Inhabited Level.Data :=
 def Level.Data.hash (c : Level.Data) : USize :=
   c.toUInt32.toUSize
 
-instance : HasBeq Level.Data :=
+instance : BEq Level.Data :=
   ⟨fun (a b : UInt64) => a == b⟩
 
 def Level.Data.depth (c : Level.Data) : UInt32 :=
@@ -201,7 +201,7 @@ def toNat (lvl : Level) : Option Nat :=
 @[extern "lean_level_eq"]
 protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
 
-instance : HasBeq Level := ⟨Level.beq⟩
+instance : BEq Level := ⟨Level.beq⟩
 
 /-- `occurs u l` return `true` iff `u` occurs in `l`. -/
 def occurs : Level → Level → Bool

stage0/src/Lean/Message.lean

@@ -94,7 +94,7 @@ protected def toString (msgData : MessageData) : IO String := do
   let fmt ← msgData.format
   pure $ toString fmt
 
-instance : HasAppend MessageData := ⟨compose⟩
+instance : Append MessageData := ⟨compose⟩
 
 instance : Coe String MessageData := ⟨ofFormat ∘ format⟩
 instance : Coe Format MessageData := ⟨ofFormat⟩
@@ -182,7 +182,7 @@ def add (msg : Message) (log : MessageLog) : MessageLog :=
 protected def append (l₁ l₂ : MessageLog) : MessageLog :=
   ⟨l₁.msgs ++ l₂.msgs⟩
 
-instance : HasAppend MessageLog :=
+instance : Append MessageLog :=
   ⟨MessageLog.append⟩
 
 def hasErrors (log : MessageLog) : Bool :=

stage0/src/Lean/Meta/AbstractMVars.lean

@@ -17,7 +17,7 @@ instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩
 def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool :=
   r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr
 
-instance : HasBeq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩
+instance : BEq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩
 
 namespace AbstractMVars
 

stage0/src/Lean/Meta/AppBuilder.lean

@@ -270,11 +270,11 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
 /--
   Similar to `mkAppM`, but it allows us to specify which arguments are provided explicitly using `Option` type.
   Example:
-  Given `Pure.pure {m : Type u → Type v} [HasPure m] {α : Type u} (a : α) : m α`,
+  Given `Pure.pure {m : Type u → Type v} [Pure m] {α : Type u} (a : α) : m α`,
   ```
   mkAppOptM `Pure.pure #[m, none, none, a]
   ```
-  returns a `Pure.pure` application if the instance `HasPure m` can be synthesized, and the universes match.
+  returns a `Pure.pure` application if the instance `Pure m` can be synthesized, and the universes match.
   Note that,
   ```
   mkAppM `Pure.pure #[a]

stage0/src/Lean/Meta/Basic.lean

@@ -78,7 +78,7 @@ namespace InfoCacheKey
 instance : Inhabited InfoCacheKey := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩
 instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩
-instance : HasBeq InfoCacheKey :=
+instance : BEq InfoCacheKey :=
   ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩
 end InfoCacheKey
 
@@ -144,8 +144,8 @@ instance : AddMessageContext MetaM := {
   let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore
   pure (a, sCore, s)
 
-instance {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
-  ⟨fun env opts x _ => MetaHasEval.eval env opts x.run' true⟩
+instance {α} [MetaEval α] : MetaEval (MetaM α) :=
+  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
 
 protected def throwIsDefEqStuck {α} : MetaM α :=
   throw $ Exception.internal isDefEqStuckExceptionId
@@ -920,10 +920,10 @@ def withMCtx {α} (mctx : MetavarContext) : n α → n α :=
 /--
   Similar to `approxDefEq`, but uses all available approximations.
   We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
-  For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`.
+  For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[Pure ?m]`.
   Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
   as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
-  solve `[HasPure (fun _ => IO Bool)]` -/
+  solve `[Pure (fun _ => IO Bool)]` -/
 @[inline] def fullApproxDefEq {α} : n α → n α :=
   mapMetaM fullApproxDefEqImp
 
@@ -991,7 +991,7 @@ def ppExpr (e : Expr) : m Format :=
   let mctx ← getMCtx
   try x catch _ => setEnv env; setMCtx mctx; y
 
-instance {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
+instance {α} : OrElse (MetaM α) := ⟨Meta.orelse⟩
 
 @[inline] private def orelseMergeErrorsImp {α} (x y : MetaM α)
     (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)

stage0/src/Lean/Meta/DiscrTree.lean

@@ -29,13 +29,14 @@ namespace Lean.Meta.DiscrTree
   discrimination tree.
 
   Recall that projections from classes are **NOT** reducible.
-  For example, the expressions `Add.add α (ringHasAdd ?α ?s) ?x ?x`
+  For example, the expressions `Add.add α (ringAdd ?α ?s) ?x ?x`
   and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys
   respctively
   ```
-  ⟨HasAdd.add, 4⟩, *, *, *, *
-  ⟨HasAdd.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩
+  ⟨Add.add, 4⟩, *, *, *, *
+  ⟨Add.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩
   ```
+
   That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`.
   We say the `Add.add` applications are the de-facto canonical forms in
   the metaprogramming framework.
@@ -61,7 +62,7 @@ def Key.lt : Key → Key → Bool
   | Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
   | k₁,              k₂              => k₁.ctorIdx < k₂.ctorIdx
 
-instance : HasLess Key := ⟨fun a b => Key.lt a b⟩
+instance : Less Key := ⟨fun a b => Key.lt a b⟩
 instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
 
 def Key.format : Key → Format
@@ -96,7 +97,7 @@ instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩
   - We ignore proofs because of proof irrelevance. It doesn't make sense to try to
     index their structure.
 
-  - We ignore instance implicit arguments (e.g., `[HasAdd α]`) because they are "morally" canonical.
+  - We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical.
     Moreover, we may have many definitionally equal terms floating around.
     Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`.
 
@@ -206,10 +207,10 @@ private partial def createNodes {α} (keys : Array Key) (v : α) (i : Nat) : Tri
   else
     Trie.node #[v] #[]
 
-private def insertVal {α} [HasBeq α] (vs : Array α) (v : α) : Array α :=
+private def insertVal {α} [BEq α] (vs : Array α) (v : α) : Array α :=
   if vs.contains v then vs else vs.push v
 
-private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
+private partial def insertAux {α} [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
   | i, Trie.node vs cs =>
     if h : i < keys.size then
       let k := keys.get ⟨i, h⟩
@@ -222,7 +223,7 @@ private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat
     else
       Trie.node (insertVal vs v) cs
 
-def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
+def insertCore {α} [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
   if keys.isEmpty then panic! "invalid key sequence"
   else
     let k := keys[0]
@@ -234,7 +235,7 @@ def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) :
       let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
-def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
+def insert {α} [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
   let keys ← mkPath e
   pure $ d.insertCore keys v
 
@@ -278,9 +279,9 @@ private def getKeyArgs (e : Expr) (isMatch? : Bool) : MetaM (Key × Array Expr)
           we may want to notify the caller that the TC problem may be solveable
           later after it assigns `?m`.
           The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
-          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (HasAdd ?m)`
+          That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
           where `?m` is a read-only metavariable, and the discrimination tree contains the keys
-          `HadAdd Nat` and `HasAdd Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
+          `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as
           a regular metavariable here, otherwise we return the empty set of candidates.
           This is incorrect because it is equivalent to saying that there is no solution even if
           the caller assigns `?m` and try again. -/

stage0/src/Lean/Meta/DiscrTreeTypes.lean

@@ -37,7 +37,7 @@ protected def Key.beq : Key → Key → Bool
   | Key.other,       Key.other       => true
   | _,                _              => false
 
-instance : HasBeq Key := ⟨Key.beq⟩
+instance : BEq Key := ⟨Key.beq⟩
 
 inductive Trie (α : Type)
   | node (vs : Array α) (children : Array (Key × Trie α)) : Trie α

stage0/src/Lean/Meta/ReduceEval.lean

@@ -10,25 +10,22 @@ import Lean.Meta.Offset
 
 namespace Lean.Meta
 
-class HasReduceEval (α : Type) :=
-  (reduceEval : Expr → MetaM α)
-
 class ReduceEval (α : Type) :=
   (reduceEval : Expr → MetaM α)
 
-def reduceEval {α : Type} [HasReduceEval α] (e : Expr) : MetaM α :=
+def reduceEval {α : Type} [ReduceEval α] (e : Expr) : MetaM α :=
   withAtLeastTransparency TransparencyMode.default $
-  HasReduceEval.reduceEval e
+  ReduceEval.reduceEval e
 
 private def throwFailedToEval {α} (e : Expr) : MetaM α :=
   throwError! "reduceEval: failed to evaluate argument{indentExpr e}"
 
-instance : HasReduceEval Nat := ⟨fun e => do
+instance : ReduceEval Nat := ⟨fun e => do
   let e ← whnf e
   let some n ← pure $ evalNat e | throwFailedToEval e
   pure n⟩
 
-instance {α : Type} [HasReduceEval α] : HasReduceEval (Option α) := ⟨fun e => do
+instance {α : Type} [ReduceEval α] : ReduceEval (Option α) := ⟨fun e => do
   let e ← whnf e
   let Expr.const c .. ← pure e.getAppFn | throwFailedToEval e
   let nargs := e.getAppNumArgs
@@ -36,7 +33,7 @@ instance {α : Type} [HasReduceEval α] : HasReduceEval (Option α) := ⟨fun e
   else if c == `Option.some && nargs == 1 then some <$> reduceEval e.appArg!
   else throwFailedToEval e⟩
 
-instance : HasReduceEval String := ⟨fun e => do
+instance : ReduceEval String := ⟨fun e => do
   let Expr.lit (Literal.strVal s) _ ← whnf e | throwFailedToEval e
   pure s⟩
 
@@ -56,6 +53,6 @@ private partial def evalName (e : Expr) : MetaM Name := do
   else
     throwFailedToEval e
 
-instance : HasReduceEval Name := ⟨evalName⟩
+instance : ReduceEval Name := ⟨evalName⟩
 
 end Lean.Meta

stage0/src/Lean/Meta/TransparencyMode.lean

@@ -17,7 +17,7 @@ def beq : TransparencyMode → TransparencyMode → Bool
   | reducible, reducible => true
   | _,         _         => false
 
-instance : HasBeq TransparencyMode := ⟨beq⟩
+instance : BEq TransparencyMode := ⟨beq⟩
 
 def hash : TransparencyMode → USize
   | all       => 7

stage0/src/Lean/MetavarContext.lean

@@ -17,14 +17,14 @@ the requirements imposed by these modules.
 - We may invoke TC while executing `isDefEq`. We need this feature to
 be able to solve unification problems such as:
 ```
-f ?a (ringHasAdd ?s) ?x ?y =?= f Int intHasAdd n m
+f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
 ```
 where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`
 During `isDefEq` (i.e., unification), it will need to solve the constrain
 ```
-ringHasAdd ?s =?= intHasAdd
+ringAdd ?s =?= intAdd
 ```
-We say `ringHasAdd ?s` is stuck because it cannot be reduced until we
+We say `ringAdd ?s` is stuck because it cannot be reduced until we
 synthesize the term `?s : Ring ?a` using TC. This can be done since we
 have assigned `?a := Int` when solving `?a =?= Int`.
 
@@ -227,7 +227,7 @@ abbrev LocalInstances := Array LocalInstance
 def LocalInstance.beq (i₁ i₂ : LocalInstance) : Bool :=
   i₁.fvar == i₂.fvar
 
-instance : HasBeq LocalInstance := ⟨LocalInstance.beq⟩
+instance : BEq LocalInstance := ⟨LocalInstance.beq⟩
 
 /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
 def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=

stage0/src/Lean/Parser/Basic.lean

@@ -158,7 +158,7 @@ instance : ToString Error := ⟨Error.toString⟩
 protected def beq (e₁ e₂ :  Error) : Bool :=
   e₁.unexpected == e₂.unexpected && e₁.expected == e₂.expected
 
-instance : HasBeq Error := ⟨Error.beq⟩
+instance : BEq Error := ⟨Error.beq⟩
 
 def merge (e₁ e₂ : Error) : Error :=
   match e₂ with
@@ -335,7 +335,7 @@ abbrev TrailingParser := Parser
   fn   := andthenFn p.fn q.fn
 }
 
-instance : HasAndthen Parser := ⟨andthen⟩
+instance : AndThen Parser := ⟨andthen⟩
 
 @[inline] def nodeFn (n : SyntaxNodeKind) (p : ParserFn) : ParserFn := fun c s =>
   let iniSz := s.stackSize
@@ -461,7 +461,7 @@ def orelseFnCore (p q : ParserFn) (mergeErrors : Bool) : ParserFn := fun c s =>
   fn   := orelseFn p.fn q.fn
 }
 
-instance : HasOrelse Parser := ⟨orelse⟩
+instance : OrElse Parser := ⟨orelse⟩
 
 @[noinline] def noFirstTokenInfo (info : ParserInfo) : ParserInfo := {
   collectTokens := info.collectTokens,
@@ -1407,7 +1407,7 @@ def insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α :=
 
 instance {α : Type} : Inhabited (TokenMap α) := ⟨RBMap.empty⟩
 
-instance {α : Type} : HasEmptyc (TokenMap α) := ⟨RBMap.empty⟩
+instance {α : Type} : EmptyCollection (TokenMap α) := ⟨RBMap.empty⟩
 
 end TokenMap
 

stage0/src/Lean/ParserCompiler.lean

@@ -86,7 +86,7 @@ match e with
       setEnv $ ctx.combinatorAttr.setDeclFor env c c'
       mkCall c'
     else
-      -- if this is a generic function, e.g. `HasAndthen.andthen`, it's easier to just unfold it until we are
+      -- if this is a generic function, e.g. `AndThen.andthen`, it's easier to just unfold it until we are
       -- back to parser combinators
       let some e' ← unfoldDefinition? e
         | throwError! "don't know how to generate {ctx.varName} for non-parser combinator '{e}'"

stage0/src/Lean/PrettyPrinter/Formatter.lean

@@ -46,7 +46,7 @@ abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State CoreM
     p₁
     (fun _ => do set s; p₂)
 
-instance {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩
+instance {α} : OrElse (FormatterM α) := ⟨FormatterM.orelse⟩
 
 abbrev Formatter := FormatterM Unit
 

stage0/src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -109,7 +109,7 @@ abbrev Parenthesizer := ParenthesizerM Unit
     p₁
     (fun _ => do set s; p₂)
 
-instance {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
+instance {α} : OrElse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
 
 unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
   KeyedDeclsAttribute.init {

stage0/src/Lean/Server.lean

@@ -97,16 +97,16 @@ def updateOpenDocuments (key : DocumentUri) (val : EditableDocument) : ServerM U
 def readLspMessage : ServerM JsonRpc.Message := fun st =>
   Lsp.readLspMessage st.hIn
 
-def readLspRequestAs (expectedMethod : String) (α : Type) [HasFromJson α] : ServerM (Request α) := fun st =>
+def readLspRequestAs (expectedMethod : String) (α : Type) [FromJson α] : ServerM (Request α) := fun st =>
   Lsp.readLspRequestAs st.hIn expectedMethod α
 
-def readLspNotificationAs (expectedMethod : String) (α : Type) [HasFromJson α] : ServerM α := fun st =>
+def readLspNotificationAs (expectedMethod : String) (α : Type) [FromJson α] : ServerM α := fun st =>
   Lsp.readLspNotificationAs st.hIn expectedMethod α
 
-def writeLspNotification {α : Type} [HasToJson α] (method : String) (params : α) : ServerM Unit := fun st =>
+def writeLspNotification {α : Type} [ToJson α] (method : String) (params : α) : ServerM Unit := fun st =>
   Lsp.writeLspNotification st.hOut method params
 
-def writeLspResponse {α : Type} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit := fun st =>
+def writeLspResponse {α : Type} [ToJson α] (id : RequestID) (params : α) : ServerM Unit := fun st =>
   Lsp.writeLspResponse st.hOut id params
 
 /-- Clears diagnostics for the document version 'version'. -/
@@ -172,13 +172,13 @@ def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit := fun st =>
 
 def handleHover (p : HoverParams) : ServerM Json := pure Json.null
 
-def parseParams (paramType : Type) [HasFromJson paramType] (params : Json) : ServerM paramType :=
+def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType :=
   match fromJson? params with
   | some parsed => pure parsed
   | none        => throw (userError "got param with wrong structure")
 
 def handleNotification (method : String) (params : Json) : ServerM Unit := do
-  let h := (fun paramType [HasFromJson paramType] (handler : paramType → ServerM Unit) =>
+  let h := (fun paramType [FromJson paramType] (handler : paramType → ServerM Unit) =>
     parseParams paramType params >>= handler)
   match method with
   | "textDocument/didOpen"   => h DidOpenTextDocumentParams handleDidOpen
@@ -188,7 +188,7 @@ def handleNotification (method : String) (params : Json) : ServerM Unit := do
   | _                        => throw (userError "got unsupported notification method")
 
 def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do
-  let h := (fun paramType responseType [HasFromJson paramType] [HasToJson responseType]
+  let h := (fun paramType responseType [FromJson paramType] [ToJson responseType]
                 (handler : paramType → ServerM responseType) =>
              parseParams paramType params >>= handler >>= writeLspResponse id)
   match method with

stage0/src/Lean/Syntax.lean

@@ -331,7 +331,7 @@ partial def structEq : Syntax → Syntax → Bool
 | Syntax.ident _ rawVal val preresolved, Syntax.ident _ rawVal' val' preresolved' => rawVal == rawVal' && val == val' && preresolved == preresolved'
 | _, _ => false
 
-instance : HasBeq Lean.Syntax := ⟨structEq⟩
+instance : BEq Lean.Syntax := ⟨structEq⟩
 
 /--
 Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right.

stage0/src/Lean/Util/MonadCache.lean

@@ -33,30 +33,30 @@ open Std (HashMap)
 
 /-- Adapter for implementing `MonadCache` interface using `HashMap`s.
     We just have to specify how to extract/modify the `HashMap`. -/
-class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [HasBeq α] [Hashable α] :=
+class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] :=
 (getCache    : m (HashMap α β))
 (modifyCache : (HashMap α β → HashMap α β) → m Unit)
 
 namespace MonadHashMapCacheAdapter
 
-@[inline] def findCached? {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
+@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
 let c ← getCache
 pure (c.find? a)
 
-@[inline] def cache {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
+@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
 modifyCache fun s => s.insert a b
 
-instance {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m :=
+instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m :=
 { findCached? := MonadHashMapCacheAdapter.findCached?,
   cache       := MonadHashMapCacheAdapter.cache }
 
 end MonadHashMapCacheAdapter
 
-def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [HasBeq α] [Hashable α] := StateRefT (HashMap α β) m
+def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m
 
 namespace MonadCacheT
 
-variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [HasBeq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
+variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
 
 instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) :=
 { getCache    := (get : StateRefT' ..),

stage0/src/Lean/Util/SCC.lean

@@ -14,7 +14,7 @@ namespace Lean.SCC
 open Std
 
 section
-variables (α : Type) [HasBeq α] [Hashable α]
+variables (α : Type) [BEq α] [Hashable α]
 
 structure Data :=
 (index?   : Option Nat := none)
@@ -30,7 +30,7 @@ structure State :=
 abbrev M := StateM (State α)
 end
 
-variables {α : Type} [HasBeq α] [Hashable α]
+variables {α : Type} [BEq α] [Hashable α]
 
 private def getDataOf (a : α) : M α Data := do
 let s ← get

stage0/src/Std/Data/AssocList.lean

@@ -17,7 +17,7 @@ variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Mon
 abbrev empty : AssocList α β :=
 nil
 
-instance : HasEmptyc (AssocList α β) := ⟨empty⟩
+instance : EmptyCollection (AssocList α β) := ⟨empty⟩
 
 abbrev insert (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
 m.cons k v
@@ -41,29 +41,29 @@ def mapVal (f : β → δ) : AssocList α β → AssocList α δ
 | nil        => nil
 | cons k v t => cons k (f v) (mapVal f t)
 
-def findEntry? [HasBeq α] (a : α) : AssocList α β → Option (α × β)
+def findEntry? [BEq α] (a : α) : AssocList α β → Option (α × β)
 | nil         => none
 | cons k v es => match k == a with
   | true  => some (k, v)
   | false => findEntry? a es
 
-def find? [HasBeq α] (a : α) : AssocList α β → Option β
+def find? [BEq α] (a : α) : AssocList α β → Option β
 | nil         => none
 | cons k v es => match k == a with
   | true  => some v
   | false => find? a es
 
-def contains [HasBeq α] (a : α) : AssocList α β → Bool
+def contains [BEq α] (a : α) : AssocList α β → Bool
 | nil         => false
 | cons k v es => k == a || contains a es
 
-def replace [HasBeq α] (a : α) (b : β) : AssocList α β → AssocList α β
+def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β
 | nil         => nil
 | cons k v es => match k == a with
   | true  => cons a b es
   | false => cons k v (replace a b es)
 
-def erase [HasBeq α] (a : α) : AssocList α β → AssocList α β
+def erase [BEq α] (a : α) : AssocList α β → AssocList α β
 | nil         => nil
 | cons k v es => match k == a with
   | true  => es

stage0/src/Std/Data/DList.lean

@@ -20,12 +20,12 @@ variables {α : Type u}
 open List
 
 def ofList (l : List α) : DList α :=
-⟨HasAppend.append l, fun t => by rw appendNil; exact rfl⟩
+⟨Append.append l, fun t => by rw appendNil; exact rfl⟩
 
 def empty : DList α :=
 ⟨id, fun t => rfl⟩
 
-instance : HasEmptyc (DList α) :=
+instance : EmptyCollection (DList α) :=
 ⟨DList.empty⟩
 
 def toList : DList α → List α
@@ -61,7 +61,7 @@ def push : DList α → α → DList α
     rw [h [a], h (a::t), appendAssoc (f []) [a] t]
     exact rfl⟩
 
-instance : HasAppend (DList α) :=
+instance : Append (DList α) :=
 ⟨DList.append⟩
 
 end DList

stage0/src/Std/Data/HashMap.lean

@@ -53,19 +53,19 @@ foldBucketsM h.buckets d f
 @[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ :=
 foldBuckets m.buckets d f
 
-def findEntry? [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
+def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
 match m with
 | ⟨_, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
   (buckets.val.uget i h).findEntry? a
 
-def find? [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
+def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
 match m with
 | ⟨_, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
   (buckets.val.uget i h).find? a
 
-def contains [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
+def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
 match m with
 | ⟨_, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -92,7 +92,7 @@ let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this
 { size    := size,
   buckets := moveEntries 0 buckets.val new_buckets }
 
-def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
+def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
 match m with
 | ⟨size, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -106,7 +106,7 @@ match m with
     then { size := size', buckets := buckets' }
     else expand size' buckets'
 
-def erase [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
+def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
 match m with
 | ⟨ size, buckets ⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -114,28 +114,28 @@ match m with
   if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
   else m
 
-inductive WellFormed [HasBeq α] [Hashable α] : HashMapImp α β → Prop
+inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop
 | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
 | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b)
 | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
-def HashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] :=
+def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
 { m : HashMapImp α β // m.WellFormed }
 
 open Std.HashMapImp
 
-def mkHashMap {α : Type u} {β : Type v} [HasBeq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
+def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
 ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashMap
-variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α]
+variables {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
 instance inhabited : Inhabited (HashMap α β) :=
 ⟨mkHashMap⟩
 
-instance hasEmptyc : HasEmptyc (HashMap α β) :=
+instance hasEmptyc : EmptyCollection (HashMap α β) :=
 ⟨mkHashMap⟩
 
 @[inline] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=

stage0/src/Std/Data/HashSet.lean

@@ -52,13 +52,13 @@ foldBucketsM h.buckets d f
 @[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
 foldBuckets m.buckets d f
 
-def find? [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
+def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
 match m with
 | ⟨_, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
   (buckets.val.uget i h).find? (fun a' => a == a')
 
-def contains [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
+def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
 match m with
 | ⟨_, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -85,7 +85,7 @@ let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;
 { size    := size,
   buckets := moveEntries 0 buckets.val new_buckets }
 
-def insert [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
 match m with
 | ⟨size, buckets⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -99,7 +99,7 @@ match m with
     then { size := size', buckets := buckets' }
     else expand size' buckets'
 
-def erase [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
 match m with
 | ⟨ size, buckets ⟩ =>
   let ⟨i, h⟩ := mkIdx buckets.property (hash a)
@@ -107,28 +107,28 @@ match m with
   if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
   else m
 
-inductive WellFormed [HasBeq α] [Hashable α] : HashSetImp α → Prop
+inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop
 | mkWff     : ∀ n,                  WellFormed (mkHashSetImp n)
 | insertWff : ∀ m a, WellFormed m → WellFormed (insert m a)
 | eraseWff  : ∀ m a, WellFormed m → WellFormed (erase m a)
 
 end HashSetImp
 
-def HashSet (α : Type u) [HasBeq α] [Hashable α] :=
+def HashSet (α : Type u) [BEq α] [Hashable α] :=
 { m : HashSetImp α // m.WellFormed }
 
 open HashSetImp
 
-def mkHashSet {α : Type u} [HasBeq α] [Hashable α] (nbuckets := 8) : HashSet α :=
+def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α :=
 ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashSet
-variables {α : Type u} [HasBeq α] [Hashable α]
+variables {α : Type u} [BEq α] [Hashable α]
 
 instance : Inhabited (HashSet α) :=
 ⟨mkHashSet⟩
 
-instance : HasEmptyc (HashSet α) :=
+instance : EmptyCollection (HashSet α) :=
 ⟨mkHashSet⟩
 
 @[inline] def insert (m : HashSet α) (a : α) : HashSet α :=

stage0/src/Std/Data/PersistentArray.lean

@@ -229,7 +229,7 @@ match n with
 
 @[specialize] def forIn (t : PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
 match (← forInAux (inh := ⟨init⟩) f t.root init) with
-| ForInStep.done b  => b
+| ForInStep.done b  => pure b
 | ForInStep.yield b =>
   for v in t.tail do
     match (← f v b) with
@@ -279,7 +279,7 @@ def append (t₁ t₂ : PersistentArray α) : PersistentArray α :=
 if t₁.isEmpty then t₂
 else t₂.foldl PersistentArray.push t₁
 
-instance : HasAppend (PersistentArray α) := ⟨append⟩
+instance : Append (PersistentArray α) := ⟨append⟩
 
 @[inline] def findSome? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
 Id.run (t.findSomeM? f)

stage0/src/Std/Data/PersistentHashMap.lean

@@ -31,21 +31,21 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
 
 end PersistentHashMap
 
-structure PersistentHashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] :=
+structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
 (root    : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray)
 (size    : Nat                        := 0)
 
-abbrev PHashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] := PersistentHashMap α β
+abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
 
 namespace PersistentHashMap
 variables {α : Type u} {β : Type v}
 
-def empty [HasBeq α] [Hashable α] : PersistentHashMap α β := {}
+def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
 
-def isEmpty [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
+def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
 m.size == 0
 
-instance [HasBeq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
+instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
 
 def mkEmptyEntries {α β} : Node α β :=
 Node.entries mkEmptyEntriesArray
@@ -76,7 +76,7 @@ have h₂ : (vs.push v).size = vs.size + 1 by apply Array.szPushEq
 have h₃ : ks.size + 1 = vs.size + 1      by rw h; exact rfl
 (h₁.trans h₃).trans h₂.symm
 
-partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
+partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β
 | n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
   if h : i < keys.size then
     let idx : Fin keys.size := ⟨i, h⟩;
@@ -89,7 +89,7 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat
     ⟨Node.collision (keys.push k) (vals.push v) (pushSizeEq heq k v), IsCollisionNode.mk _ _ _⟩
 | ⟨Node.entries _, h⟩, _, _, _ => False.elim (nomatch h)
 
-def insertAtCollisionNode [HasBeq α] : CollisionNode α β → α → β → CollisionNode α β :=
+def insertAtCollisionNode [BEq α] : CollisionNode α β → α → β → CollisionNode α β :=
 fun n k v => insertAtCollisionNodeAux n 0 k v
 
 def getCollisionNodeSize : CollisionNode α β → Nat
@@ -103,7 +103,7 @@ let vs : Array β := Array.mkEmpty maxCollisions
 let vs := (vs.push v₁).push v₂
 Node.collision ks vs rfl
 
-partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
+partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
 | Node.collision keys vals heq, _, depth, k, v =>
   let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
   if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
@@ -130,10 +130,10 @@ partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize
       if k == k' then Entry.entry k v
       else Entry.ref $ mkCollisionNode k' v' k v
 
-def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
+def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
 | { root := n, size := sz }, k, v => { root := insertAux n (hash k) 1 k v, size := sz + 1 }
 
-partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
+partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
 | i, k =>
   if h : i < keys.size then
     let k' := keys.get ⟨i, h⟩
@@ -141,7 +141,7 @@ partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : key
     else findAtAux keys vals heq (i+1) k
   else none
 
-partial def findAux [HasBeq α] : Node α β → USize → α → Option β
+partial def findAux [BEq α] : Node α β → USize → α → Option β
 | Node.entries entries, h, k =>
   let j     := (mod2Shift h shift).toNat
   match entries.get! j with
@@ -150,21 +150,21 @@ partial def findAux [HasBeq α] : Node α β → USize → α → Option β
   | Entry.entry k' v => if k == k' then some v else none
 | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option β
+def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
 | { root := n, .. }, k => findAux n (hash k) k
 
-@[inline] def getOp [HasBeq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
+@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
 self.find? idx
 
-@[inline] def findD [HasBeq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
+@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
 (m.find? a).getD b₀
 
-@[inline] def find! [HasBeq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
+@[inline] def find! [BEq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
 match m.find? a with
 | some b => b
 | none   => panic! "key is not in the map"
 
-partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β)
+partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β)
 | i, k =>
   if h : i < keys.size then
     let k' := keys.get ⟨i, h⟩
@@ -172,7 +172,7 @@ partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq
     else findEntryAtAux keys vals heq (i+1) k
   else none
 
-partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option (α × β)
+partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β)
 | Node.entries entries, h, k =>
   let j     := (mod2Shift h shift).toNat
   match entries.get! j with
@@ -181,10 +181,10 @@ partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option (
   | Entry.entry k' v => if k == k' then some (k', v) else none
 | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
+def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
 | { root := n, .. }, k => findEntryAux n (hash k) k
 
-partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
+partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
 | i, k =>
   if h : i < keys.size then
     let k' := keys.get ⟨i, h⟩
@@ -192,7 +192,7 @@ partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq :
     else containsAtAux keys vals heq (i+1) k
   else false
 
-partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
+partial def containsAux [BEq α] : Node α β → USize → α → Bool
 | Node.entries entries, h, k =>
   let j     := (mod2Shift h shift).toNat
   match entries.get! j with
@@ -201,7 +201,7 @@ partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
   | Entry.entry k' v => k == k'
 | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
 
-def contains [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Bool
+def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
 | { root := n, .. }, k => containsAux n (hash k) k
 
 partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Option (α × β) → Option (α × β)
@@ -225,7 +225,7 @@ def isUnaryNode : Node α β → Option (α × β)
   else
     none
 
-partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β × Bool
+partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bool
 | n@(Node.collision keys vals heq), _, k =>
   match keys.indexOf? k with
   | some idx =>
@@ -249,7 +249,7 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
       | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
       | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
 
-def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
+def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
 | { root := n, size := sz }, k =>
   let h := hash k
   let (n, del) := eraseAux n h k
@@ -276,17 +276,17 @@ variables {σ : Type w}
   | Entry.ref node  => foldlMAux f node acc)
   acc
 
-@[specialize] def foldlM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
+@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ :=
 foldlMAux f map.root acc
 
-@[specialize] def forM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
+@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
 map.foldlM (fun _ => f) ⟨⟩
 
-@[specialize] def foldl [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (acc : σ) : σ :=
+@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (acc : σ) : σ :=
 Id.run $ map.foldlM f acc
 end
 
-def toList [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) :=
+def toList [BEq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) :=
 m.foldl (fun ps k v => (k, v) :: ps) []
 
 structure Stats :=
@@ -313,7 +313,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
     | Entry.entry _ _ => stats)
     stats
 
-def stats [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
+def stats [BEq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
 collectStats m.root {} 1
 
 def Stats.toString (s : Stats) : String :=

stage0/src/Std/Data/PersistentHashSet.lean

@@ -8,14 +8,14 @@ import Std.Data.PersistentHashMap
 namespace Std
 universes u v
 
-structure PersistentHashSet (α : Type u) [HasBeq α] [Hashable α] :=
+structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] :=
 (set : PersistentHashMap α Unit)
 
-abbrev PHashSet (α : Type u) [HasBeq α] [Hashable α] := PersistentHashSet α
+abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
 
 namespace PersistentHashSet
 
-variables {α : Type u} [HasBeq α] [Hashable α]
+variables {α : Type u} [BEq α] [Hashable α]
 
 @[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
 s.set.isEmpty
@@ -26,7 +26,7 @@ s.set.isEmpty
 instance : Inhabited (PersistentHashSet α) :=
 ⟨empty⟩
 
-instance : HasEmptyc (PersistentHashSet α) :=
+instance : EmptyCollection (PersistentHashSet α) :=
 ⟨empty⟩
 
 @[inline] def insert (s : PersistentHashSet α) (a : α) : PersistentHashSet α :=

stage0/src/Std/Data/RBMap.lean

@@ -217,7 +217,7 @@ def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v)
 @[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt :=
   mkRBMap ..
 
-instance (α : Type u) (β : Type v) (lt : α → α → Bool) : HasEmptyc (RBMap α β lt) :=
+instance (α : Type u) (β : Type v) (lt : α → α → Bool) : EmptyCollection (RBMap α β lt) :=
   ⟨RBMap.empty⟩
 
 namespace RBMap

stage0/src/Std/Data/RBTree.lean

@@ -13,7 +13,7 @@ def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=
 @[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt :=
   mkRBMap α Unit lt
 
-instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) :=
+instance (α : Type u) (lt : α → α → Bool) : EmptyCollection (RBTree α lt) :=
   ⟨mkRBTree α lt⟩
 
 namespace RBTree

stage0/stdlib/Init/Control/EState.c

@@ -21,7 +21,6 @@ lean_object* l_EStateM_run_x27_match__1(lean_object*, lean_object*, lean_object*
 lean_object* l_EStateM_tryCatch(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9_match__3___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__9;
-lean_object* l_EStateM_orelse_x27___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_EStateM_seqRight___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__6;
 lean_object* l_EStateM_Init_Control_EState___instance__7___closed__3;
@@ -30,7 +29,6 @@ lean_object* l_EStateM_modifyGet_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5(lean_object*, lean_object*);
 lean_object* l_EStateM_run(lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_x27_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_seqRight_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_fromStateM___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -38,20 +36,21 @@ lean_object* l_EStateM_dummyRestore___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_bind_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_x27_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_dummySave(lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_EStateM_seqRight_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__8___rarg(lean_object*);
+lean_object* l_EStateM_orElse_x27___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_EStateM_adaptExcept(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_dummySave___boxed(lean_object*, lean_object*);
 lean_object* l_EStateM_dummyRestore(lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_modifyGet_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_adaptExcept_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_map_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___closed__1;
 lean_object* l_EStateM_dummyRestore___rarg___boxed(lean_object*, lean_object*);
@@ -69,13 +68,13 @@ lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_fromStateM_match__1___rarg(lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__4___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_modifyGet___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_map(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__3(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Except_toString___rarg___closed__2;
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__10;
+lean_object* l_EStateM_orElse_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_bind_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_map_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -83,11 +82,12 @@ lean_object* l_EStateM_Init_Control_EState___instance__9_match__1___rarg(lean_ob
 lean_object* l_EStateM_modifyGet(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_nonBacktrackable___closed__1;
 lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_x27_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_nonBacktrackable___closed__2;
 lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_x27_match__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__7___closed__2;
 lean_object* l_EStateM_fromStateM(lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_x27_match__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_seqRight(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__1_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -101,15 +101,16 @@ lean_object* l_EStateM_Init_Control_EState___instance__1___rarg___closed__2;
 lean_object* l_EStateM_adaptExcept___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__7___closed__4;
 lean_object* l_EStateM_Init_Control_EState___instance__7(lean_object*, lean_object*);
-lean_object* l_EStateM_orelse___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_set(lean_object*, lean_object*);
 lean_object* l_EStateM_pure(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9_match__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__8(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_run_x27(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_x27_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_set___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__9_match__3(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__3___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__7;
 lean_object* l_EStateM_Init_Control_EState___instance__4(lean_object*, lean_object*, lean_object*);
@@ -118,7 +119,6 @@ lean_object* l_EStateM_Init_Control_EState___instance__5___closed__3;
 lean_object* l_EStateM_Init_Control_EState___instance__6___rarg(lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__1_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__7___closed__1;
-lean_object* l_EStateM_orelse_x27_match__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_bind(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_throw(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__2_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -127,11 +127,11 @@ lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__1;
 lean_object* l_EStateM_Init_Control_EState___instance__2_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__2;
+lean_object* l_EStateM_orElse_x27(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_run_x27_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__5___closed__8;
-lean_object* l_EStateM_orelse_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_EStateM_orelse_x27(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_EStateM_orElse_x27_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_tryCatch___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EStateM_Init_Control_EState___instance__1_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
@@ -542,7 +542,7 @@ x_4 = lean_alloc_closure((void*)(l_EStateM_tryCatch___rarg), 5, 0);
 return x_4;
 }
 }
-lean_object* l_EStateM_orelse_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_EStateM_orElse_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -566,15 +566,15 @@ return x_7;
 }
 }
 }
-lean_object* l_EStateM_orelse_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
-x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_match__1___rarg), 3, 0);
+x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_match__1___rarg), 3, 0);
 return x_5;
 }
 }
-lean_object* l_EStateM_orelse___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
@@ -605,15 +605,15 @@ return x_11;
 }
 }
 }
-lean_object* l_EStateM_orelse(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
-x_5 = lean_alloc_closure((void*)(l_EStateM_orelse___rarg), 4, 0);
+x_5 = lean_alloc_closure((void*)(l_EStateM_orElse___rarg), 4, 0);
 return x_5;
 }
 }
-lean_object* l_EStateM_orelse_x27_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_EStateM_orElse_x27_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -637,15 +637,15 @@ return x_7;
 }
 }
 }
-lean_object* l_EStateM_orelse_x27_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse_x27_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
-x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27_match__1___rarg), 3, 0);
+x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27_match__1___rarg), 3, 0);
 return x_5;
 }
 }
-lean_object* l_EStateM_orelse_x27_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_EStateM_orElse_x27_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -669,15 +669,15 @@ return x_7;
 }
 }
 }
-lean_object* l_EStateM_orelse_x27_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse_x27_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
-x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27_match__2___rarg), 3, 0);
+x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27_match__2___rarg), 3, 0);
 return x_5;
 }
 }
-lean_object* l_EStateM_orelse_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
+lean_object* l_EStateM_orElse_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; lean_object* x_7; lean_object* x_8; 
@@ -764,21 +764,21 @@ return x_21;
 }
 }
 }
-lean_object* l_EStateM_orelse_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_EStateM_orElse_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
 lean_object* x_5; 
-x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27___rarg___boxed), 5, 0);
+x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27___rarg___boxed), 5, 0);
 return x_5;
 }
 }
-lean_object* l_EStateM_orelse_x27___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_EStateM_orElse_x27___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 uint8_t x_6; lean_object* x_7; 
 x_6 = lean_unbox(x_4);
 lean_dec(x_4);
-x_7 = l_EStateM_orelse_x27___rarg(x_1, x_2, x_3, x_6, x_5);
+x_7 = l_EStateM_orElse_x27___rarg(x_1, x_2, x_3, x_6, x_5);
 return x_7;
 }
 }
@@ -1644,7 +1644,7 @@ lean_object* l_EStateM_Init_Control_EState___instance__6___rarg(lean_object* x_1
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_EStateM_orelse___rarg), 4, 1);
+x_2 = lean_alloc_closure((void*)(l_EStateM_orElse___rarg), 4, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }

stage0/stdlib/Init/Core.c

@@ -100,14 +100,12 @@ lean_object* l_Classical_typeDecidable_match__1___rarg___boxed(lean_object*, lea
 lean_object* l_Init_Core___instance__1;
 lean_object* l_Init_Core___instance__3(lean_object*);
 lean_object* l_Init_Core___instance__14_match__1___rarg(lean_object*, lean_object*);
-lean_object* l_default_sizeof(lean_object*, lean_object*);
 lean_object* l_cond___rarg(uint8_t, lean_object*, lean_object*);
 lean_object* l_Quotient_recOnSubsingleton___rarg(lean_object*, lean_object*);
 lean_object* l_Task_get___boxed(lean_object*, lean_object*);
 lean_object* l_Init_Core___instance__24_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_False_elim(lean_object*, uint8_t);
 lean_object* l_Init_Core___instance__45_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_default_sizeof___boxed(lean_object*, lean_object*);
 lean_object* l_Task_map___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_prio;
 lean_object* l_Init_Core___instance__45_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
@@ -165,7 +163,6 @@ lean_object* l_ite(lean_object*, lean_object*);
 lean_object* l_Quot_hrecOn(lean_object*, lean_object*, lean_object*);
 lean_object* l_not___boxed(lean_object*);
 lean_object* l_Task_Priority_dedicated;
-lean_object* l_default_sizeof_match__1___rarg(lean_object*, lean_object*);
 uint8_t l_Init_Core___instance__31;
 lean_object* l_std_prec_arrow;
 uint8_t l_Init_Core___instance__22___rarg(uint8_t, uint8_t);
@@ -214,7 +211,6 @@ lean_object* l_decEq(lean_object*);
 lean_object* l_Subtype_Init_Core___instance__42_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_or___boxed(lean_object*, lean_object*);
 uint8_t l_strictOr(uint8_t, uint8_t);
-lean_object* l_default_sizeof_match__1(lean_object*, lean_object*);
 lean_object* l_Eq_mpr___rarg(lean_object*);
 lean_object* l_decEq___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_inferInstance(lean_object*);
@@ -313,6 +309,7 @@ lean_object* l_Function_const(lean_object*, lean_object*);
 lean_object* l_Lean_reduceNat___boxed(lean_object*);
 lean_object* l_and_match__1(lean_object*);
 lean_object* l_and_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*);
+lean_object* l_default_sizeOf___boxed(lean_object*, lean_object*);
 lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Function_combine(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Init_Core___instance__25_match__1(lean_object*);
@@ -349,8 +346,10 @@ lean_object* l_id(lean_object*);
 lean_object* l_Subtype_Init_Core___instance__41(lean_object*, lean_object*);
 lean_object* l_inline___rarg(lean_object*);
 lean_object* l_dite___rarg___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_default_sizeOf_match__1(lean_object*, lean_object*);
 lean_object* l_id___rarg(lean_object*);
 lean_object* l_Init_Core___instance__32;
+lean_object* l_default_sizeOf(lean_object*, lean_object*);
 lean_object* l_arbitrary(lean_object*);
 lean_object* l_Eq_ndrec___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Init_Core___instance__24(lean_object*);
@@ -390,6 +389,7 @@ lean_object* l_Eq_ndrecOn(lean_object*, lean_object*, lean_object*, lean_object*
 lean_object* l_Init_Core___instance__44___rarg(lean_object*, lean_object*);
 lean_object* lean_task_get_own(lean_object*);
 uint8_t l_decidableOfDecidableOfIff___rarg(uint8_t, lean_object*);
+lean_object* l_default_sizeOf_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_cast___rarg(lean_object*);
 lean_object* l_Function_onFun___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_thunk_bind(lean_object*, lean_object*);
@@ -902,7 +902,7 @@ x_6 = lean_task_bind(x_3, x_4, x_5);
 return x_6;
 }
 }
-lean_object* l_default_sizeof_match__1___rarg(lean_object* x_1, lean_object* x_2) {
+lean_object* l_default_sizeOf_match__1___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -910,15 +910,15 @@ x_3 = lean_apply_1(x_2, x_1);
 return x_3;
 }
 }
-lean_object* l_default_sizeof_match__1(lean_object* x_1, lean_object* x_2) {
+lean_object* l_default_sizeOf_match__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_default_sizeof_match__1___rarg), 2, 0);
+x_3 = lean_alloc_closure((void*)(l_default_sizeOf_match__1___rarg), 2, 0);
 return x_3;
 }
 }
-lean_object* l_default_sizeof(lean_object* x_1, lean_object* x_2) {
+lean_object* l_default_sizeOf(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -926,11 +926,11 @@ x_3 = lean_unsigned_to_nat(0u);
 return x_3;
 }
 }
-lean_object* l_default_sizeof___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_default_sizeOf___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_default_sizeof(x_1, x_2);
+x_3 = l_default_sizeOf(x_1, x_2);
 lean_dec(x_2);
 return x_3;
 }
@@ -939,7 +939,7 @@ static lean_object* _init_l_Init_Core___instance__3___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_default_sizeof___boxed), 2, 1);
+x_1 = lean_alloc_closure((void*)(l_default_sizeOf___boxed), 2, 1);
 lean_closure_set(x_1, 0, lean_box(0));
 return x_1;
 }

stage0/stdlib/Lean/Delaborator.c

@@ -343,6 +343,7 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabDiv___closed__4;
 lean_object* l___regBuiltin_Lean_Delaborator_delabBind(lean_object*);
 lean_object* l_Lean_Delaborator_delabMap___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabBAnd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_evalNat___closed__9;
 extern lean_object* l_Lean_mkAppStx___closed__8;
 lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Delaborator_delabFor___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabCoe___closed__1;
@@ -426,6 +427,7 @@ lean_object* l_Array_anyRangeMAux___at_Lean_Delaborator_delabAppExplicit___spec_
 lean_object* l_Lean_Delaborator_delabSort___closed__10;
 lean_object* l___regBuiltin_Lean_Delaborator_delabCons(lean_object*);
 lean_object* l_Lean_Delaborator_delabTuple___lambda__1___closed__4;
+extern lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__7;
 lean_object* l_Lean_Delaborator_delabBOr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_orelse(lean_object*);
 lean_object* l_Lean_Delaborator_delabBNe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -582,6 +584,7 @@ lean_object* l_Lean_Delaborator_delabPrefixOp___lambda__1(lean_object*, lean_obj
 lean_object* l_Lean_Delaborator_getPPOption(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabTuple___closed__3;
+extern lean_object* l_Lean_Meta_evalNat___closed__12;
 lean_object* l_Lean_Delaborator_annotatePos_match__2(lean_object*);
 lean_object* l_Lean_Delaborator_delabProd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_getPPUnicode(lean_object*);
@@ -613,7 +616,6 @@ lean_object* l_Lean_Delaborator_delabModN___lambda__1___closed__4;
 extern lean_object* l_Lean_mkAppStx___closed__6;
 lean_object* l_Lean_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabEq___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___regBuiltin_Lean_Delaborator_delabLT___closed__4;
 lean_object* l___regBuiltin_Lean_Delaborator_delabOrElse___closed__1;
 lean_object* l_Lean_getRevAliases(lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabOrElse___closed__2;
@@ -688,6 +690,7 @@ lean_object* l_Lean_Delaborator_delabProjectionApp_match__2___rarg(lean_object*,
 lean_object* l___regBuiltin_Lean_Delaborator_delabGE___closed__2;
 lean_object* l_Lean_Delaborator_delabModN___lambda__1___closed__1;
 lean_object* l_Lean_getPPCoercions___closed__2;
+extern lean_object* l_Lean_Meta_evalNat___closed__5;
 lean_object* l___regBuiltin_Lean_Delaborator_delabseq___closed__2;
 lean_object* l_Lean_Delaborator_delabGT___lambda__1___closed__3;
 lean_object* l_Lean_Delaborator_delabProjectionApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -761,7 +764,6 @@ lean_object* l_Lean_Delaborator_delabProd___lambda__1___closed__4;
 lean_object* l_Lean_LocalDecl_type(lean_object*);
 uint8_t l_Lean_getPPNotation(lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabAdd___closed__2;
-lean_object* l___regBuiltin_Lean_Delaborator_delabMul___closed__4;
 lean_object* l_Lean_Delaborator_failure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Init_LeanInit___instance__19___rarg___closed__1;
 lean_object* l_Lean_Delaborator_delabStructureInstance_match__2(lean_object*);
@@ -863,7 +865,6 @@ lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__2___closed__2;
 lean_object* lean_panic_fn(lean_object*, lean_object*);
 extern lean_object* l_Lean_setOptionFromString___closed__1;
 lean_object* l_Lean_getPPUniverses___closed__2;
-lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5;
 lean_object* l_Lean_Delaborator_delabLT___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
 extern lean_object* l_Lean_Init_LeanInit___instance__8___closed__1;
@@ -928,7 +929,6 @@ lean_object* l_Lean_Delaborator_getExprKind_match__1___rarg(lean_object*, lean_o
 lean_object* l_Lean_getPPStructureInstanceType___closed__2;
 lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__3___closed__2;
 lean_object* l_Lean_Delaborator_delabGE___lambda__1___closed__3;
-lean_object* l___regBuiltin_Lean_Delaborator_delabLE___closed__4;
 lean_object* l_Lean_getPPExplicit___boxed(lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabNot(lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_elabMData___closed__1;
@@ -1018,7 +1018,6 @@ lean_object* l_Lean_Delaborator_delabProjectionApp_match__3___rarg(lean_object*,
 lean_object* l___regBuiltin_Lean_Delaborator_delabAndM___closed__1;
 lean_object* l_Lean_Delaborator_delabHEq___lambda__1___closed__6;
 lean_object* l_Lean_Delaborator_delabLetE___closed__4;
-lean_object* l___regBuiltin_Lean_Delaborator_delabAdd___closed__4;
 lean_object* l___regBuiltin_Lean_Delaborator_delabBVar___closed__1;
 lean_object* l_Lean_Delaborator_delabModN(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabPow___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1081,7 +1080,6 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabTuple___closed__1;
 lean_object* l_Lean_Delaborator_delabStructureInstance_match__3___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_List_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_getPPBinderTypes___closed__2;
-lean_object* l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4;
 lean_object* l_Lean_Delaborator_liftMetaM(lean_object*);
 lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabseq___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1174,7 +1172,6 @@ lean_object* l_Lean_Delaborator_delabMapRev___lambda__1___boxed(lean_object*, le
 lean_object* l___regBuiltin_Lean_Delaborator_delabLE___closed__2;
 lean_object* l___regBuiltin_Lean_Delaborator_delabBNe___closed__2;
 lean_object* l_Lean_Delaborator_delabseqRight___lambda__1___closed__3;
-lean_object* l___regBuiltin_Lean_Delaborator_delabSub___closed__4;
 lean_object* l_Lean_Delaborator_delabAndM___lambda__1___closed__1;
 lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkAppStx___closed__1;
@@ -19104,32 +19101,24 @@ return x_7;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasOfNat");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_evalNat___closed__9;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1;
 x_2 = l_Lean_Expr_isCharLit___closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -19142,8 +19131,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -22931,32 +22920,24 @@ return x_11;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasAdd");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__7;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__1;
 x_2 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__5;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -22969,8 +22950,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -23051,32 +23032,24 @@ return x_11;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasSub");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_evalNat___closed__12;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabSub___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabSub___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabSub___closed__1;
 x_2 = l_Lean_Meta_evalNat___closed__14;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -23089,8 +23062,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabSub___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabSub___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabSub___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabSub___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -23171,32 +23144,24 @@ return x_11;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasMul");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_evalNat___closed__5;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabMul___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabMul___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabMul___closed__1;
 x_2 = l_Lean_Meta_evalNat___closed__7;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -23209,8 +23174,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabMul___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabMul___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabMul___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabMul___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -23300,7 +23265,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabDiv___closed__1()
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasDiv");
+x_1 = lean_mk_string("Div");
 return x_1;
 }
 }
@@ -23428,7 +23393,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMod___closed__1()
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasMod");
+x_1 = lean_mk_string("Mod");
 return x_1;
 }
 }
@@ -23564,7 +23529,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabModN___closed__1(
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasModN");
+x_1 = lean_mk_string("ModN");
 return x_1;
 }
 }
@@ -23708,7 +23673,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabPow___closed__1()
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasPow");
+x_1 = lean_mk_string("Pow");
 return x_1;
 }
 }
@@ -23883,32 +23848,24 @@ return x_11;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasLessEq");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_mkLe___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabLE___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabLE___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabLE___closed__1;
 x_2 = l_Lean_Meta_mkLe___rarg___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -23921,8 +23878,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabLE___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabLE___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabLE___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabLE___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -24185,32 +24142,24 @@ return x_11;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__1() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasLess");
-return x_1;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Delaborator_getExprKind___closed__5;
+x_2 = l_Lean_Meta_mkLt___rarg___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l___regBuiltin_Lean_Delaborator_delabLT___closed__1;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___regBuiltin_Lean_Delaborator_delabLT___closed__2;
+x_1 = l___regBuiltin_Lean_Delaborator_delabLT___closed__1;
 x_2 = l_Lean_Meta_mkLt___rarg___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__4() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -24223,8 +24172,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabLT___closed__3;
-x_4 = l___regBuiltin_Lean_Delaborator_delabLT___closed__4;
+x_3 = l___regBuiltin_Lean_Delaborator_delabLT___closed__2;
+x_4 = l___regBuiltin_Lean_Delaborator_delabLT___closed__3;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -24676,7 +24625,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabBEq___closed__1()
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasBeq");
+x_1 = lean_mk_string("BEq");
 return x_1;
 }
 }
@@ -25088,7 +25037,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasEquiv");
+x_1 = lean_mk_string("Equiv");
 return x_1;
 }
 }
@@ -25105,22 +25054,14 @@ return x_3;
 static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("Equiv");
-return x_1;
-}
-}
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__2;
-x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3;
+x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5() {
+static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() {
 _start:
 {
 lean_object* x_1; 
@@ -25133,8 +25074,8 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Delaborator_delabAttribute;
-x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4;
-x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5;
+x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3;
+x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
@@ -25900,7 +25841,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAppend___closed__
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasAppend");
+x_1 = lean_mk_string("Append");
 return x_1;
 }
 }
@@ -26156,7 +26097,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAndThen___closed_
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasAndthen");
+x_1 = lean_mk_string("AndThen");
 return x_1;
 }
 }
@@ -26292,7 +26233,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabBind___closed__1(
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasBind");
+x_1 = lean_mk_string("Bind");
 return x_1;
 }
 }
@@ -26436,7 +26377,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseq___closed__1()
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasSeq");
+x_1 = lean_mk_string("Seq");
 return x_1;
 }
 }
@@ -26572,7 +26513,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseqLeft___closed_
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasSeqLeft");
+x_1 = lean_mk_string("SeqLeft");
 return x_1;
 }
 }
@@ -26708,7 +26649,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseqRight___closed
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasSeqRight");
+x_1 = lean_mk_string("SeqRight");
 return x_1;
 }
 }
@@ -27098,7 +27039,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOrElse___closed__
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("HasOrelse");
+x_1 = lean_mk_string("OrElse");
 return x_1;
 }
 }
@@ -28213,8 +28154,6 @@ l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2 = _init_l___regBuiltin_Le
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2);
 l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3);
-l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabOfNat(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28346,8 +28285,6 @@ l___regBuiltin_Lean_Delaborator_delabAdd___closed__2 = _init_l___regBuiltin_Lean
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__2);
 l___regBuiltin_Lean_Delaborator_delabAdd___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__3);
-l___regBuiltin_Lean_Delaborator_delabAdd___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabAdd(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28363,8 +28300,6 @@ l___regBuiltin_Lean_Delaborator_delabSub___closed__2 = _init_l___regBuiltin_Lean
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__2);
 l___regBuiltin_Lean_Delaborator_delabSub___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__3);
-l___regBuiltin_Lean_Delaborator_delabSub___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabSub(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28380,8 +28315,6 @@ l___regBuiltin_Lean_Delaborator_delabMul___closed__2 = _init_l___regBuiltin_Lean
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__2);
 l___regBuiltin_Lean_Delaborator_delabMul___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__3);
-l___regBuiltin_Lean_Delaborator_delabMul___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabMul(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28487,8 +28420,6 @@ l___regBuiltin_Lean_Delaborator_delabLE___closed__2 = _init_l___regBuiltin_Lean_
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__2);
 l___regBuiltin_Lean_Delaborator_delabLE___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__3);
-l___regBuiltin_Lean_Delaborator_delabLE___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabLE(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28531,8 +28462,6 @@ l___regBuiltin_Lean_Delaborator_delabLT___closed__2 = _init_l___regBuiltin_Lean_
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__2);
 l___regBuiltin_Lean_Delaborator_delabLT___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__3);
-l___regBuiltin_Lean_Delaborator_delabLT___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__4();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__4);
 res = l___regBuiltin_Lean_Delaborator_delabLT(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@@ -28664,8 +28593,6 @@ l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3 = _init_l___regBuiltin_Le
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3);
 l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4();
 lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4);
-l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5();
-lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5);
 res = l___regBuiltin_Lean_Delaborator_delabEquiv(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);

stage0/stdlib/Lean/Elab/Do.c

@@ -123,7 +123,6 @@ extern lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchA
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_resolveLocalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_299____closed__20;
-lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58;
 uint8_t l_Array_anyRangeMAux___at_Lean_Elab_Term_Do_hasTerminalAction___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__5___closed__2;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTermCore(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -220,7 +219,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0_
 lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__16;
 lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__5___closed__8;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__12;
-lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__1___closed__8;
 lean_object* l_Lean_Elab_Term_Do_extendUpdatedVarsAux_update(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -486,7 +484,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore(lean_object*, l
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_Do_getDoLetRecVars___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_getDoLetArrowVars___closed__3;
 extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__41;
-lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54;
 lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__12;
 extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__3;
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -612,7 +609,6 @@ size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53;
 lean_object* l_Lean_Elab_Term_Do_concat___closed__3;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__6;
-lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
 lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_concatWith(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
 lean_object* l_Lean_Elab_Term_Do_CodeBlock_uvars___default;
@@ -793,7 +789,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTermCore___closed__7;
 lean_object* l_Array_iterateMAux___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___closed__7;
 lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBNode_any___at_Lean_Elab_Term_Do_extendUpdatedVars___spec__1(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57;
 lean_object* l_Array_umapMAux___at_Lean_Elab_Term_Do_ToTerm_mkJoinPointCore___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___at_Lean_Elab_Term_Do_extendUpdatedVarsAux_update___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___at_Lean_Elab_Term_Do_eraseVars___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -27803,71 +27798,19 @@ return x_3;
 static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("HasPure");
-return x_1;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52;
-x_2 = l_Lean_Meta_mkPure___rarg___closed__3;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53;
-x_3 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_3, 0, x_2);
-lean_ctor_set(x_3, 1, x_1);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54;
-x_3 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_3, 0, x_2);
-lean_ctor_set(x_3, 1, x_1);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_IO_Prim_fopenFlags___closed__4;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57() {
+static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_IO_Prim_fopenFlags___closed__4;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56;
+x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@@ -27875,7 +27818,7 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58() {
+static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -29501,7 +29444,7 @@ x_930 = lean_array_push(x_909, x_929);
 x_931 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__50;
 x_932 = l_Lean_addMacroScope(x_881, x_931, x_880);
 x_933 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_934 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_934 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_935 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_935, 0, x_885);
 lean_ctor_set(x_935, 1, x_933);
@@ -29688,7 +29631,7 @@ x_1036 = lean_array_push(x_1015, x_1035);
 x_1037 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__50;
 x_1038 = l_Lean_addMacroScope(x_987, x_1037, x_986);
 x_1039 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1040 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1040 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1041 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1041, 0, x_991);
 lean_ctor_set(x_1041, 1, x_1039);
@@ -29936,7 +29879,7 @@ lean_inc(x_1093);
 lean_inc(x_1094);
 x_1175 = l_Lean_addMacroScope(x_1094, x_1174, x_1093);
 x_1176 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1177 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1177 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1178 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1178, 0, x_1098);
 lean_ctor_set(x_1178, 1, x_1176);
@@ -30243,7 +30186,7 @@ lean_inc(x_1266);
 lean_inc(x_1267);
 x_1348 = l_Lean_addMacroScope(x_1267, x_1347, x_1266);
 x_1349 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1350 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1350 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1351 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1351, 0, x_1271);
 lean_ctor_set(x_1351, 1, x_1349);
@@ -30557,7 +30500,7 @@ lean_inc(x_1440);
 lean_inc(x_1441);
 x_1522 = l_Lean_addMacroScope(x_1441, x_1521, x_1440);
 x_1523 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1524 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1524 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1525 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1525, 0, x_1445);
 lean_ctor_set(x_1525, 1, x_1523);
@@ -30610,9 +30553,9 @@ lean_ctor_set(x_1550, 1, x_1548);
 lean_ctor_set(x_1550, 2, x_1547);
 lean_ctor_set(x_1550, 3, x_1549);
 x_1551 = lean_array_push(x_1448, x_1550);
-x_1552 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58;
+x_1552 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53;
 x_1553 = l_Lean_addMacroScope(x_1441, x_1552, x_1440);
-x_1554 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57;
+x_1554 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52;
 x_1555 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1555, 0, x_1445);
 lean_ctor_set(x_1555, 1, x_1554);
@@ -30850,7 +30793,7 @@ lean_inc(x_1604);
 lean_inc(x_1605);
 x_1686 = l_Lean_addMacroScope(x_1605, x_1685, x_1604);
 x_1687 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1688 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1688 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1689 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1689, 0, x_1609);
 lean_ctor_set(x_1689, 1, x_1687);
@@ -30903,9 +30846,9 @@ lean_ctor_set(x_1714, 1, x_1712);
 lean_ctor_set(x_1714, 2, x_1711);
 lean_ctor_set(x_1714, 3, x_1713);
 x_1715 = lean_array_push(x_1612, x_1714);
-x_1716 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58;
+x_1716 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53;
 x_1717 = l_Lean_addMacroScope(x_1605, x_1716, x_1604);
-x_1718 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57;
+x_1718 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52;
 x_1719 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1719, 0, x_1609);
 lean_ctor_set(x_1719, 1, x_1718);
@@ -31147,7 +31090,7 @@ lean_inc(x_1769);
 lean_inc(x_1770);
 x_1851 = l_Lean_addMacroScope(x_1770, x_1850, x_1769);
 x_1852 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_1853 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_1853 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_1854 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_1854, 0, x_1774);
 lean_ctor_set(x_1854, 1, x_1852);
@@ -31504,7 +31447,7 @@ lean_inc(x_1969);
 lean_inc(x_1970);
 x_2051 = l_Lean_addMacroScope(x_1970, x_2050, x_1969);
 x_2052 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
-x_2053 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55;
+x_2053 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30;
 x_2054 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_2054, 0, x_1974);
 lean_ctor_set(x_2054, 1, x_2052);
@@ -46278,16 +46221,6 @@ l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52 = _init_l_Lean_Ela
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52);
 l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53();
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53);
-l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54);
-l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55);
-l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56);
-l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57);
-l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58();
-lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58);
 l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default = _init_l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default();
 lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default);
 l_Lean_Elab_Term_Do_ToCodeBlock_Context_insideFor___default = _init_l_Lean_Elab_Term_Do_ToCodeBlock_Context_insideFor___default();

stage0/stdlib/Lean/Meta/DiscrTree.c

@@ -5166,7 +5166,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__2;
 x_2 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__3;
-x_3 = lean_unsigned_to_nat(226u);
+x_3 = lean_unsigned_to_nat(227u);
 x_4 = lean_unsigned_to_nat(23u);
 x_5 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__4;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);