chore: update stage0

2020-03-02 08:42:07 -08:00 · 2020-03-02 08:42:07 -08:00 · f607e9c478
commit f607e9c478
parent 0893b62598
18 changed files with 6128 additions and 3894 deletions
--- a/stage0/src/Init/Control/State.lean
+++ b/stage0/src/Init/Control/State.lean
@ -23,6 +23,10 @@ Prod.fst <$> x s

@[reducible] def StateM (σ α : Type u) : Type u := StateT σ Id α

+instance StateM.subsingleton {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) :=
+⟨λ x y => funext $ fun (s : σ) => match x s, y s with
+  | (a₁, s₁), (a₂, s₂) => Subsingleton.elim a₁ a₂ ▸ Subsingleton.elim s₁ s₂ ▸ rfl⟩
+
 namespace StateT
 section
 variables {σ : Type u} {m : Type u → Type v}
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@ -1682,6 +1682,21 @@ fun y x => f x y

 end Function

+/- Squash -/
+
+def Squash (α : Type u) := Quot (fun (a b : α) => True)
+
+def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
+
+theorem Squash.ind {α : Type u} {β : Squash α → Prop} (h : ∀ (a : α), β (Squash.mk a)) : ∀ (q : Squash α), β q :=
+Quot.ind h
+
+@[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
+Quot.lift f (fun a b _ => Subsingleton.elim _ _) s
+
+instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
+⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩
+
 /- Classical reasoning support -/

 namespace Classical
--- a/stage0/src/Init/Data/HashSet.lean
+++ b/stage0/src/Init/Data/HashSet.lean
@ -4,18 +4,128 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.HashMap
+import Init.Data.Array.Basic
+import Init.Data.List.Control
+import Init.Data.Option.Basic
+import Init.Data.Hashable
+universes u v w

-universes u v
+def HashSetBucket (α : Type u) :=
+{ b : Array (List α) // b.size > 0 }

-structure HashSet (α : Type u) [HasBeq α] [Hashable α] :=
-(set : HashMap α Unit)
+def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α :=
+⟨ data.val.uset i d h,
+  transRelRight Greater (Array.szFSetEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩
+
+structure HashSetImp (α : Type u) :=
+(size       : Nat)
+(buckets    : HashSetBucket α)
+
+def mkHashSetImp {α : Type u} (nbuckets := 8) : HashSetImp α :=
+let n := if nbuckets = 0 then 8 else nbuckets;
+{ size       := 0,
+  buckets    :=
+  ⟨ mkArray n [],
+    have p₁ : (mkArray n ([] : List α)).size = n from Array.szMkArrayEq _ _;
+    have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl;
+    have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from
+      match nbuckets with
+      | 0            => Nat.zeroLtSucc _
+      | (Nat.succ x) => Nat.zeroLtSucc _;
+    transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
+
+namespace HashSetImp
+variables {α : Type u}
+
+def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
+⟨u %ₙ n, USize.modnLt _ h⟩
+
+@[inline] def reinsertAux (hashFn : α → USize) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
+let ⟨i, h⟩ := mkIdx data.property (hashFn a);
+data.update i (a :: data.val.uget i h) h
+
+@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
+data.val.foldlM (fun d as => as.foldlM f d) d
+
+@[inline] def foldBuckets {δ : Type w} (data : HashSetBucket α) (d : δ) (f : δ → α → δ) : δ :=
+Id.run $ foldBucketsM data d f
+
+@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (d : δ) (h : HashSetImp α) : m δ :=
+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 α :=
+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 :=
+match m with
+| ⟨_, buckets⟩ =>
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
+  (buckets.val.uget i h).contains a
+
+-- TODO: remove `partial` by using well-founded recursion
+partial def moveEntries [Hashable α] : Nat → Array (List α) → HashSetBucket α → HashSetBucket α
+| i, source, target =>
+  if h : i < source.size then
+     let idx : Fin source.size := ⟨i, h⟩;
+     let es  : List α   := source.get idx;
+     -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
+     let source                := source.set idx [];
+     let target                := es.foldl (reinsertAux hash) target;
+     moveEntries (i+1) source target
+  else target
+
+def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
+let nbuckets := buckets.val.size * 2;
+have aux₁  : nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero);
+have aux₂  : (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _;
+let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], aux₂.symm ▸ aux₁⟩;
+{ size    := size,
+  buckets := moveEntries 0 buckets.val new_buckets }
+
+def insert [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+match m with
+| ⟨size, buckets⟩ =>
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
+  let bkt    := buckets.val.uget i h;
+  if bkt.contains a
+  then ⟨size, buckets.update i (bkt.replace a a) h⟩
+  else
+    let size'    := size + 1;
+    let buckets' := buckets.update i (a :: bkt) h;
+    if size' ≤ buckets.val.size
+    then { size := size', buckets := buckets' }
+    else expand size' buckets'
+
+def erase [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+match m with
+| ⟨ size, buckets ⟩ =>
+  let ⟨i, h⟩ := mkIdx buckets.property (hash a);
+  let bkt    := buckets.val.uget i h;
+  if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
+  else m
+
+inductive WellFormed [HasBeq α] [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 α] :=
+{ m : HashSetImp α // m.WellFormed }
+
+open HashSetImp

 def mkHashSet {α : Type u} [HasBeq α] [Hashable α] (nbuckets := 8) : HashSet α :=
-{ set := mkHashMap nbuckets }
+⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩

 namespace HashSet
-
 variables {α : Type u} [HasBeq α] [Hashable α]

 instance : Inhabited (HashSet α) :=
@ -24,33 +134,47 @@ instance : Inhabited (HashSet α) :=
 instance : HasEmptyc (HashSet α) :=
 ⟨mkHashSet⟩

-@[inline] def insert (s : HashSet α) (a : α) : HashSet α :=
-{ set := s.set.insert a () }
+@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
+match m with
+| ⟨ m, hw ⟩ => ⟨ m.insert a, WellFormed.insertWff m a hw ⟩

-@[inline] def erase (s : HashSet α) (a : α) : HashSet α :=
-{ set := s.set.erase a }
+@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
+match m with
+| ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩

-@[inline] def find? (s : HashSet α) (a : α) : Option α :=
-match s.set.findEntry? a with
-| some (k, _) => some k
-| none        => none
+@[inline] def find? (m : HashSet α) (a : α) : Option α :=
+match m with
+| ⟨ m, _ ⟩ => m.find? a

-@[inline] def contains (s : HashSet α) (a : α) : Bool :=
-s.set.contains a
+@[inline] def contains (m : HashSet α) (a : α) : Bool :=
+match m with
+| ⟨ m, _ ⟩ => m.contains a

-@[inline] def size (s : HashSet α) : Nat :=
-s.set.size
+@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (d : δ) (h : HashSet α) : m δ :=
+match h with
+| ⟨ h, _ ⟩ => h.foldM f d

-@[inline] def isEmpty (s : HashSet α) : Bool :=
-s.set.isEmpty
+@[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSet α) : δ :=
+match m with
+| ⟨ m, _ ⟩ => m.fold f d
+
+@[inline] def size (m : HashSet α) : Nat :=
+match m with
+| ⟨ {size := sz, ..}, _ ⟩ => sz
+
+@[inline] def isEmpty (m : HashSet α) : Bool :=
+m.size = 0

@[inline] def empty : HashSet α :=
 mkHashSet

-@[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : HashSet α) : m β :=
-s.set.foldM (fun d a _ => f d a) d
+def toList (m : HashSet α) : List α :=
+m.fold (fun r a => a::r) []

-@[inline] def fold {β : Type v} (f : β → α → β) (d : β) (s : HashSet α) : β :=
-Id.run $ s.foldM f d
+def toArray (m : HashSet α) : Array α :=
+m.fold (fun r a => r.push a) #[]
+
+def numBuckets (m : HashSet α) : Nat :=
+m.val.buckets.val.size

 end HashSet
--- a/stage0/src/Init/Data/List/Basic.lean
+++ b/stage0/src/Init/Data/List/Basic.lean
@ -165,6 +165,12 @@ def findSome? (f : α → Option β) : List α → Option β
  | some b => some b
  | none   => findSome? as

+def replace [HasBeq α] : 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
 | []    => false
 | b::bs => match a == b with
--- a/stage0/src/Init/Util.lean
+++ b/stage0/src/Init/Util.lean
@ -47,18 +47,29 @@ k (ptrAddrUnsafe a)
@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
 if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()

+inductive PtrEqResult {α : Type u} (x y : α) : Type
+| unknown {}           : PtrEqResult
+| yesEqual (h : x = y) : PtrEqResult
+
+@[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
+if ptrAddrUnsafe a == ptrAddrUnsafe b then k (PtrEqResult.yesEqual lcProof) else k PtrEqResult.unknown
+
@[implementedBy withPtrEqUnsafe]
 def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
 k ()

-- `withPtrEq` for `DecidableEq`
-
+/-- `withPtrEq` for `DecidableEq` -/
@[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
 let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsingEqTrue (k ()));
 condEq b
  (fun h => isTrue (ofBoolUsingEqTrue h))
  (fun h => isFalse (ofBoolUsingEqFalse h))

+/-- Similar to `withPtrEq`, but executes the continuation `k` with the "result" of the pointer equality test. -/
+@[implementedBy withPtrEqResultUnsafe]
+def withPtrEqResult {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
+k PtrEqResult.unknown
+
@[implementedBy withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
 k 0
--- a/stage0/src/runtime/sharecommon.cpp
+++ b/stage0/src/runtime/sharecommon.cpp
@ -25,10 +25,6 @@ extern "C" uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
    return memcmp(reinterpret_cast<char*>(o1) + header_sz, reinterpret_cast<char*>(o2) + header_sz, sz1 - header_sz) == 0;
 }

-extern "C" uint8 lean_maxsharing_eq(b_obj_arg o1, b_obj_arg o2) {
-    return lean_sharecommon_eq(o1, o2);
-}
-
 extern "C" usize lean_sharecommon_hash(b_obj_arg o) {
    lean_assert(!lean_is_scalar(o));
    size_t sz = lean_object_byte_size(o);
@ -39,10 +35,6 @@ extern "C" usize lean_sharecommon_hash(b_obj_arg o) {
    return hash_str(sz - header_sz, reinterpret_cast<char const *>(o) + header_sz, init);
 }

-extern "C" usize lean_maxsharing_hash(b_obj_arg o) {
-    return lean_sharecommon_hash(o);
-}
-
 // unsafe def mkObjectMap : Unit → ObjectMap
 extern "C" obj_res lean_mk_object_map(obj_arg);
 // unsafe def ObjectMap.find? (m : ObjectMap) (k : Object) : Option Object
@ -87,14 +79,6 @@ extern "C" obj_res lean_sharecommon_mk_pstate(obj_arg) {
    return mk_pair(lean_mk_object_pmap(lean_box(0)), lean_mk_object_pset(lean_box(0)));
 }

-extern "C" obj_res lean_maxsharing_mk_state(obj_arg) {
-    return mk_pair(lean_mk_object_map(lean_box(0)), lean_mk_object_set(lean_box(0)));
-}
-
-extern "C" obj_res lean_maxsharing_mk_pstate(obj_arg) {
-    return mk_pair(lean_mk_object_pmap(lean_box(0)), lean_mk_object_pset(lean_box(0)));
-}
-
 class sharecommon_state_core {
 protected:
    object * m_map;
@ -344,14 +328,4 @@ extern "C" obj_res lean_state_sharecommon(obj_arg s, obj_arg a) {
 extern "C" obj_res lean_persistent_state_sharecommon(obj_arg s, obj_arg a) {
    return sharecommon_fn<sharecommon_pstate>(s)(a);
 }
-
-// def State.maxSharing {α} (s : State) (a : α) : α × State
-extern "C" obj_res lean_state_maxsharing(obj_arg s, obj_arg a) {
-    return sharecommon_fn<sharecommon_state>(s)(a);
-}
-
-// def PersistentState.maxSharing {α} (s : PersistentState) (a : α) : α × PersistentState
-extern "C" obj_res lean_persistent_state_maxsharing(obj_arg s, obj_arg a) {
-    return sharecommon_fn<sharecommon_pstate>(s)(a);
-}
 };
--- a/stage0/src/shell/lean.cpp
+++ b/stage0/src/shell/lean.cpp
@ -380,6 +380,13 @@ std::string olean_of_lean(std::string const & lean_fn) {
 }
 }

+void check_optarg(char const * option_name) {
+    if (!optarg) {
+        std::cerr << "error: argument missing for option '-" << option_name << "'" << std::endl;
+        std::exit(1);
+    }
+}
+
 int main(int argc, char ** argv) {
 #if defined(LEAN_EMSCRIPTEN)
    EM_ASM(
@ -459,9 +466,11 @@ int main(int argc, char ** argv) {
                display_help(std::cout);
                return 0;
            case 'c':
+                check_optarg("c");
                c_output = optarg;
                break;
            case 'C':
+                check_optarg("C");
                c_output = optarg;
                break;
            case 's':
@ -481,12 +490,15 @@ int main(int argc, char ** argv) {
                }
                break;
            case 'M':
+                check_optarg("M");
                opts = opts.update(get_max_memory_opt_name(), static_cast<unsigned>(atoi(optarg)));
                break;
            case 'T':
+                check_optarg("T");
                opts = opts.update(get_timeout_opt_name(), static_cast<unsigned>(atoi(optarg)));
                break;
            case 't':
+                check_optarg("t");
                trust_lvl = atoi(optarg);
                break;
            case 'q':
@ -500,6 +512,7 @@ int main(int argc, char ** argv) {
                break;
            case 'D':
                try {
+                    check_optarg("D");
                    opts = set_config_option(opts, optarg);
                } catch (lean::exception & ex) {
                    std::cerr << ex.what() << std::endl;
@ -517,6 +530,7 @@ int main(int argc, char ** argv) {
                break;
 #if defined(LEAN_DEBUG)
            case 'B':
+                check_optarg("B");
                lean::enable_debug(optarg);
                break;
 #endif
@ -524,6 +538,7 @@ int main(int argc, char ** argv) {
                new_frontend = true;
                break;
            case 'p':
+                check_optarg("p");
                load_plugin(optarg);
                break;
            default:
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
@ -39,6 +39,7 @@ lean_object* l_PSigma_HasSizeof(lean_object*, lean_object*);
 lean_object* l_Quotient_recOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_bne___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_lift___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Squash_mk___rarg___boxed(lean_object*);
 lean_object* l_Nat_HasOne;
 lean_object* l_idRhs___rarg___boxed(lean_object*);
 lean_object* l_arbitrary___rarg___boxed(lean_object*);
@ -129,6 +130,7 @@ lean_object* l_setoidHasEquiv(lean_object*, lean_object*);
 lean_object* l_PUnit_sizeof(lean_object*);
 lean_object* l_Iff_Decidable(lean_object*, lean_object*);
 lean_object* l_Nat_HasSizeof;
+lean_object* l_Squash_lift___rarg(lean_object*, lean_object*);
 lean_object* l_Ne_Decidable___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Sum_inhabitedLeft___rarg(lean_object*);
 lean_object* l_Quotient_lift_u2082___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -189,6 +191,7 @@ lean_object* l_inferInstance(lean_object*);
 lean_object* l_decidableOfDecidableOfEq(lean_object*, lean_object*);
 lean_object* l_typedExpr(lean_object*);
 lean_object* l_Bool_sizeof___boxed(lean_object*);
+lean_object* l_Squash_mk(lean_object*);
 lean_object* l_PSigma_sizeof___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_sizeof(lean_object*);
 lean_object* l_bit0(lean_object*);
@ -206,6 +209,7 @@ lean_object* l_bit1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_implies_Decidable___rarg(uint8_t, uint8_t);
 lean_object* l_typedExpr___rarg(lean_object*);
 lean_object* l_idRhs___rarg(lean_object*);
+lean_object* l_Squash_lift(lean_object*, lean_object*, lean_object*);
 lean_object* l_Prop_Inhabited;
 lean_object* l_inferInstanceAs___rarg(lean_object*);
 lean_object* l_Eq_mp(lean_object*, lean_object*, lean_object*);
@ -308,6 +312,7 @@ lean_object* l_implies_Decidable(lean_object*, lean_object*);
 uint8_t l_strictAnd(uint8_t, uint8_t);
 lean_object* l_Quotient_liftOn_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PSigma_HasSizeof___rarg(lean_object*, lean_object*);
+lean_object* l_Squash_mk___rarg(lean_object*);
 lean_object* l_Thunk_pure___boxed(lean_object*, lean_object*);
 lean_object* l_decidableOfDecidableOfIff(lean_object*, lean_object*);
 lean_object* l_bit0___rarg(lean_object*, lean_object*);
@ -3574,6 +3579,46 @@ x_4 = lean_alloc_closure((void*)(l_Function_swap___rarg), 3, 0);
 return x_4;
 }
 }
+lean_object* l_Squash_mk___rarg(lean_object* x_1) {
+_start:
+{
+lean_inc(x_1);
+return x_1;
+}
+}
+lean_object* l_Squash_mk(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Squash_mk___rarg___boxed), 1, 0);
+return x_2;
+}
+}
+lean_object* l_Squash_mk___rarg___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Squash_mk___rarg(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Squash_lift___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_apply_1(x_2, x_1);
+return x_3;
+}
+}
+lean_object* l_Squash_lift(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_Squash_lift___rarg), 2, 0);
+return x_4;
+}
+}
 static bool _G_initialized = false;
 lean_object* initialize_Init_Core(lean_object* w) {
 lean_object * res;
--- a/stage0/stdlib/Init/Data/HashSet.c
+++ b/stage0/stdlib/Init/Data/HashSet.c
--- a/stage0/stdlib/Init/Data/List/Basic.c
+++ b/stage0/stdlib/Init/Data/List/Basic.c
@ -16,6 +16,7 @@ extern "C" {
 lean_object* l_List_reverse___rarg(lean_object*);
 lean_object* l_List_HasAppend(lean_object*);
 lean_object* l_List_erase___main___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_List_replace(lean_object*);
 lean_object* l_List_foldl___main(lean_object*, lean_object*);
 lean_object* l_List_isEqv___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_eraseDupsAux___main___rarg(lean_object*, lean_object*, lean_object*);
@ -52,6 +53,7 @@ lean_object* l_List_isPrefixOf___main(lean_object*);
 lean_object* l_List_filterAux___main___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_reverseAux(lean_object*);
 lean_object* l_List_lengthAux___rarg___boxed(lean_object*, lean_object*);
+lean_object* l_List_replace___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_List_isSuffixOf___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_List_isPrefixOf___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_isPrefixOf___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -126,6 +128,7 @@ lean_object* l_List_init___rarg(lean_object*);
 lean_object* l_List_isSuffixOf(lean_object*);
 uint8_t l_List_or(lean_object*);
 uint8_t l_List_isPrefixOf___main___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_List_replace___main(lean_object*);
 lean_object* l_List_replicate(lean_object*);
 lean_object* l_List_isPrefixOf___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_lengthAux___main___rarg___boxed(lean_object*, lean_object*);
@ -177,6 +180,7 @@ lean_object* l_List_partitionAux(lean_object*);
 lean_object* l_List_isEmpty(lean_object*);
 lean_object* l_List_drop___rarg(lean_object*, lean_object*);
 lean_object* l_List_take___rarg___boxed(lean_object*, lean_object*);
+lean_object* l_List_replace___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_span___rarg(lean_object*, lean_object*);
 lean_object* l_List_hasDecEq___main(lean_object*);
 lean_object* l_List_erase(lean_object*);
@ -1880,6 +1884,109 @@ x_3 = lean_alloc_closure((void*)(l_List_findSome_x3f___rarg), 2, 0);
 return x_3;
 }
 }
+lean_object* l_List_replace___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+if (lean_obj_tag(x_2) == 0)
+{
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_2;
+}
+else
+{
+uint8_t x_5; 
+x_5 = !lean_is_exclusive(x_2);
+if (x_5 == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; 
+x_6 = lean_ctor_get(x_2, 0);
+x_7 = lean_ctor_get(x_2, 1);
+lean_inc(x_1);
+lean_inc(x_3);
+lean_inc(x_6);
+x_8 = lean_apply_2(x_1, x_6, x_3);
+x_9 = lean_unbox(x_8);
+lean_dec(x_8);
+if (x_9 == 0)
+{
+lean_object* x_10; 
+x_10 = l_List_replace___main___rarg(x_1, x_7, x_3, x_4);
+lean_ctor_set(x_2, 1, x_10);
+return x_2;
+}
+else
+{
+lean_dec(x_6);
+lean_dec(x_3);
+lean_dec(x_1);
+lean_ctor_set(x_2, 0, x_4);
+return x_2;
+}
+}
+else
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; 
+x_11 = lean_ctor_get(x_2, 0);
+x_12 = lean_ctor_get(x_2, 1);
+lean_inc(x_12);
+lean_inc(x_11);
+lean_dec(x_2);
+lean_inc(x_1);
+lean_inc(x_3);
+lean_inc(x_11);
+x_13 = lean_apply_2(x_1, x_11, x_3);
+x_14 = lean_unbox(x_13);
+lean_dec(x_13);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; 
+x_15 = l_List_replace___main___rarg(x_1, x_12, x_3, x_4);
+x_16 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_16, 0, x_11);
+lean_ctor_set(x_16, 1, x_15);
+return x_16;
+}
+else
+{
+lean_object* x_17; 
+lean_dec(x_11);
+lean_dec(x_3);
+lean_dec(x_1);
+x_17 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_17, 0, x_4);
+lean_ctor_set(x_17, 1, x_12);
+return x_17;
+}
+}
+}
+}
+}
+lean_object* l_List_replace___main(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_List_replace___main___rarg), 4, 0);
+return x_2;
+}
+}
+lean_object* l_List_replace___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_List_replace___main___rarg(x_1, x_2, x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_List_replace(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_List_replace___rarg), 4, 0);
+return x_2;
+}
+}
 uint8_t l_List_elem___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
--- a/stage0/stdlib/Init/Lean/Elab/Definition.c
+++ b/stage0/stdlib/Init/Lean/Elab/Definition.c
@ -96,6 +96,7 @@ lean_object* l_Lean_Elab_Command_elabDefLike___lambda__2___boxed(lean_object*, l
 uint8_t l_Lean_Elab_Command_DefKind_isTheorem(uint8_t);
 extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
 lean_object* l_Lean_Elab_Command_sortDeclLevelParams(lean_object*, lean_object*);
+extern lean_object* l_HashSet_Inhabited___closed__1;
 lean_object* l_Lean_Elab_Command_elabDefVal___closed__3;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabDefLike___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDefLike___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -124,7 +125,6 @@ lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lea
 lean_object* l_Lean_Elab_Command_removeUnused___closed__1;
 uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
-extern lean_object* l_HashMap_Inhabited___closed__1;
 uint8_t l_Lean_Elab_Command_DefKind_isDefOrOpaque(uint8_t);
 lean_object* lean_task_pure(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_7__mkTermState(lean_object*);
@ -848,7 +848,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_HashMap_Inhabited___closed__1;
+x_2 = l_HashSet_Inhabited___closed__1;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
@ -1342,7 +1342,7 @@ lean_object* _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_HashMap_Inhabited___closed__1;
+x_1 = l_HashSet_Inhabited___closed__1;
 x_2 = l_Array_empty___closed__1;
 x_3 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_3, 0, x_1);
--- a/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
+++ b/stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
@ -302,6 +302,7 @@ lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
 lean_object* l_Lean_ConstantInfo_type(lean_object*);
 lean_object* l_Lean_MessageData_joinSep___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_State_inhabited;
+extern lean_object* l_HashSet_Inhabited___closed__1;
 lean_object* l_HashMapImp_find_x3f___at_Lean_Elab_Tactic_evalTactic___main___spec__5(lean_object*, lean_object*);
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalTraceState___closed__1;
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalIntros(lean_object*);
@ -502,7 +503,6 @@ extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__1;
 lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalNestedTacticBlockCurly___closed__2;
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Tactic_getFVarIds___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_getMainModule(lean_object*);
-extern lean_object* l_HashMap_Inhabited___closed__1;
 lean_object* l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg___closed__1;
 extern lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__2;
 lean_object* l_List_foldl___main___at_Lean_Elab_Tactic_tagUntaggedGoals___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1647,7 +1647,7 @@ lean_object* _init_l_Lean_Elab_Tactic_collectMVars___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_HashMap_Inhabited___closed__1;
+x_1 = l_HashSet_Inhabited___closed__1;
 x_2 = l_Array_empty___closed__1;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
--- a/stage0/stdlib/Init/Lean/MetavarContext.c
+++ b/stage0/stdlib/Init/Lean/MetavarContext.c
@ -23,12 +23,14 @@ lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21_
 size_t l_USize_add(size_t, size_t);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_14__getInScope___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_23__abstractRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_HashSetImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_8__dep___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_foldlFromMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__42___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_containsAux___main___at_Lean_MetavarContext_isLevelAssigned___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_MetavarContext_assignExprCore___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_toString___at_Lean_MetavarContext_MkBinding_Exception_toString___spec__2(lean_object*);
 lean_object* l_ReaderT_lift___at_Lean_MetavarContext_MkBinding_Lean_MonadHashMapCacheAdapter___spec__1(lean_object*);
+lean_object* l_mkHashSetImp___rarg(lean_object*);
 lean_object* l_Lean_MetavarContext_MkBinding_Lean_MonadHashMapCacheAdapter___closed__2;
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l_mkHashMap___at_Lean_MetavarContext_instantiateMVars___spec__1(lean_object*);
@ -74,6 +76,7 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_MetavarContext_setMVarKind___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_assignDelayed___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
 lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
+lean_object* l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_11__reduceLocalContext(lean_object*, lean_object*);
 lean_object* lean_mk_metavar_ctx(lean_object*);
 lean_object* l_PersistentArray_anyM___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__23___boxed(lean_object*, lean_object*);
@ -216,6 +219,7 @@ lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
 uint8_t lean_metavar_ctx_is_expr_assigned(lean_object*, lean_object*);
 extern lean_object* l_Lean_LocalContext_Inhabited___closed__2;
 extern lean_object* l_PersistentArray_getAux___main___rarg___closed__1;
+uint8_t l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_LevelMVarToParam_mkParamName___rarg(lean_object*, lean_object*);
 lean_object* lean_expr_lower_loose_bvars(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_MetavarContext_findDecl_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -290,7 +294,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Expr_2__mkAppRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getDelayedAssignment_x3f___spec__1___boxed(lean_object*, lean_object*);
-uint8_t l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
 lean_object* lean_metavar_ctx_assign_expr(lean_object*, lean_object*, lean_object*);
 uint8_t l_PersistentArray_anyM___at_Lean_MetavarContext_localDeclDependsOn___spec__20(lean_object*, lean_object*);
@ -332,7 +335,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_findDecl_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_mkHashMap___at_Lean_MetavarContext_findExprDependsOn___spec__2(lean_object*);
 size_t l_Lean_Expr_hash(lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__18___boxed(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__48___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -407,6 +409,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDepen
 uint8_t l_Lean_Expr_isLambda(lean_object*);
 uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_MetavarContext_isLevelAssigned___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at_Lean_MetavarContext_exprDependsOn___spec__9___boxed(lean_object*, lean_object*);
+extern lean_object* l_HashSet_Inhabited___closed__1;
 lean_object* l_ReaderT_bind___at_Lean_MetavarContext_MkBinding_Lean_MonadHashMapCacheAdapter___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_expr_update_proj(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -414,7 +417,6 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_assig
 uint8_t l_Array_anyRangeMAux___main___at_Lean_MetavarContext_exprDependsOn___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t l_USize_land(size_t, size_t);
 lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
-lean_object* l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_findLevelDepth_x3f___boxed(lean_object*, lean_object*);
 uint8_t l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__12(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_exprDependsOn___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -440,9 +442,8 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_assig
 lean_object* l_Lean_MetavarContext_MkBinding_Exception_hasToString;
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__5(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_exprDependsOn___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_AssocList_foldlM___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(lean_object*, lean_object*);
+lean_object* l_HashSetImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_hasAssignedLevelMVar___main___boxed(lean_object*, lean_object*);
 lean_object* l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_2__visit___spec__8(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_hasAssignableLevelMVar___main___boxed(lean_object*, lean_object*);
@ -461,7 +462,6 @@ lean_object* l_Lean_Expr_withAppAux___main___at___private_Init_Lean_MetavarConte
 lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_assignLevel___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__8(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Lean_MetavarContext_MkBinding_preserveOrder(uint8_t, lean_object*);
-lean_object* l_HashMapImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_hasAssignableMVar___boxed(lean_object*, lean_object*);
 uint8_t l_PersistentHashMap_containsAux___main___at_Lean_MetavarContext_isLevelAssigned___spec__2(lean_object*, size_t, lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at_Lean_MetavarContext_exprDependsOn___spec__3___boxed(lean_object*, lean_object*);
@ -489,7 +489,6 @@ lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*);
 uint8_t l_Lean_MetavarContext_hasAssignableLevelMVar(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_isExprAssigned___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-uint8_t l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(lean_object*, lean_object*);
 uint8_t l_Lean_Name_isAnonymous(lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at_Lean_MetavarContext_localDeclDependsOn___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDependsOn___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -501,6 +500,7 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
 lean_object* lean_metavar_ctx_assign_level(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_addLevelMVarDecl___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__19___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_foldl___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_MetavarContext_assignLevel___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_foldlFromM___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__40(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__51(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -508,11 +508,10 @@ lean_object* l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__co
 lean_object* l_PersistentHashMap_containsAux___main___at_Lean_MetavarContext_isExprAssigned___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_incDepth(lean_object*);
 lean_object* l_Lean_MetavarContext_localDeclDependsOn___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDependsOn___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_withAppAux___main___at_Lean_MetavarContext_InstantiateExprMVars_main___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyM___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_HashMapImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_renameMVar___closed__1;
 lean_object* l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_exprDependsOn___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
@ -556,6 +555,7 @@ lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getExprAssignment_x3f___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__24___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_mkLet(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
+lean_object* l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDependsOn___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyM___at_Lean_MetavarContext_localDeclDependsOn___spec__32___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_getLevelDepth(lean_object*, lean_object*);
@ -595,6 +595,7 @@ lean_object* l_Lean_LocalContext_foldlM___at_Lean_MetavarContext_instantiateLCtx
 lean_object* l_Lean_MetavarContext_MkBinding_preserveOrder___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_20__anyDependsOn___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDependsOn___spec__30___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_HashSetImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_isLevelAssignable___closed__1;
 lean_object* l_Array_indexOfAux___main___at_Lean_MetavarContext_eraseDelayed___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_findExprDependsOn___closed__1;
@ -635,7 +636,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*,
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_getLevelDepth___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
-lean_object* l_HashMapImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkLevelParam(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_instantiateLCtxMVars___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_InstantiateExprMVars_instantiateLevelMVars(lean_object*, lean_object*);
@ -650,6 +650,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_MetavarContext_localDeclDepen
 extern lean_object* l_HashMap_Inhabited___closed__1;
 lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_addLevelMVarDecl___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__50___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_DependsOn_main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_mkBinding___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_hasFVar(lean_object*);
@ -695,6 +696,7 @@ lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext
 lean_object* l_HashMapImp_find_x3f___at___private_Init_Lean_MetavarContext_2__visit___spec__1(lean_object*, lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__33___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_localDeclDependsOn___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_findDecl_x3f___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
 uint8_t l_PersistentArray_anyM___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__35(lean_object*, lean_object*);
@ -13722,7 +13724,7 @@ return x_45;
 }
 }
 }
-uint8_t l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(lean_object* x_1, lean_object* x_2) {
+uint8_t l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
@ -13735,8 +13737,8 @@ else
 {
 lean_object* x_4; lean_object* x_5; uint8_t x_6; 
 x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 2);
-x_6 = lean_expr_eqv(x_4, x_1);
+x_5 = lean_ctor_get(x_2, 1);
+x_6 = lean_expr_eqv(x_1, x_4);
 if (x_6 == 0)
 {
 x_2 = x_5;
@ -13751,7 +13753,7 @@ return x_8;
 }
 }
 }
-uint8_t l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
+uint8_t l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; lean_object* x_7; uint8_t x_8; 
@ -13761,12 +13763,12 @@ x_5 = l_Lean_Expr_hash(x_2);
 x_6 = lean_usize_modn(x_5, x_4);
 lean_dec(x_4);
 x_7 = lean_array_uget(x_3, x_6);
-x_8 = l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_7);
+x_8 = l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_7);
 lean_dec(x_7);
 return x_8;
 }
 }
-lean_object* l_AssocList_foldlM___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(lean_object* x_1, lean_object* x_2) {
+lean_object* l_List_foldl___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
@ -13781,13 +13783,13 @@ if (x_3 == 0)
 {
 lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; 
 x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 2);
+x_5 = lean_ctor_get(x_2, 1);
 x_6 = lean_array_get_size(x_1);
 x_7 = l_Lean_Expr_hash(x_4);
 x_8 = lean_usize_modn(x_7, x_6);
 lean_dec(x_6);
 x_9 = lean_array_uget(x_1, x_8);
-lean_ctor_set(x_2, 2, x_9);
+lean_ctor_set(x_2, 1, x_9);
 x_10 = lean_array_uset(x_1, x_8, x_2);
 x_1 = x_10;
 x_2 = x_5;
@ -13795,32 +13797,29 @@ goto _start;
 }
 else
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
 x_12 = lean_ctor_get(x_2, 0);
 x_13 = lean_ctor_get(x_2, 1);
-x_14 = lean_ctor_get(x_2, 2);
-lean_inc(x_14);
 lean_inc(x_13);
 lean_inc(x_12);
 lean_dec(x_2);
-x_15 = lean_array_get_size(x_1);
-x_16 = l_Lean_Expr_hash(x_12);
-x_17 = lean_usize_modn(x_16, x_15);
-lean_dec(x_15);
-x_18 = lean_array_uget(x_1, x_17);
-x_19 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_19, 0, x_12);
-lean_ctor_set(x_19, 1, x_13);
-lean_ctor_set(x_19, 2, x_18);
-x_20 = lean_array_uset(x_1, x_17, x_19);
-x_1 = x_20;
-x_2 = x_14;
+x_14 = lean_array_get_size(x_1);
+x_15 = l_Lean_Expr_hash(x_12);
+x_16 = lean_usize_modn(x_15, x_14);
+lean_dec(x_14);
+x_17 = lean_array_uget(x_1, x_16);
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_12);
+lean_ctor_set(x_18, 1, x_17);
+x_19 = lean_array_uset(x_1, x_16, x_18);
+x_1 = x_19;
+x_2 = x_13;
 goto _start;
 }
 }
 }
 }
-lean_object* l_HashMapImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_HashSetImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -13839,7 +13838,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_obj
 x_6 = lean_array_fget(x_2, x_1);
 x_7 = lean_box(0);
 x_8 = lean_array_fset(x_2, x_1, x_7);
-x_9 = l_AssocList_foldlM___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(x_3, x_6);
+x_9 = l_List_foldl___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__6(x_3, x_6);
 x_10 = lean_unsigned_to_nat(1u);
 x_11 = lean_nat_add(x_1, x_10);
 lean_dec(x_1);
@ -13850,7 +13849,7 @@ goto _start;
 }
 }
 }
-lean_object* l_HashMapImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(lean_object* x_1, lean_object* x_2) {
+lean_object* l_HashSetImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
@ -13861,188 +13860,181 @@ lean_dec(x_3);
 x_6 = lean_box(0);
 x_7 = lean_mk_array(x_5, x_6);
 x_8 = lean_unsigned_to_nat(0u);
-x_9 = l_HashMapImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(x_8, x_2, x_7);
+x_9 = l_HashSetImp_moveEntries___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__5(x_8, x_2, x_7);
 x_10 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_10, 0, x_1);
 lean_ctor_set(x_10, 1, x_9);
 return x_10;
 }
 }
-lean_object* l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-if (lean_obj_tag(x_3) == 0)
+if (lean_obj_tag(x_1) == 0)
 {
-lean_dec(x_2);
-lean_dec(x_1);
-return x_3;
-}
-else
-{
-uint8_t x_4; 
-x_4 = !lean_is_exclusive(x_3);
-if (x_4 == 0)
-{
-lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; 
-x_5 = lean_ctor_get(x_3, 0);
-x_6 = lean_ctor_get(x_3, 1);
-x_7 = lean_ctor_get(x_3, 2);
-x_8 = lean_expr_eqv(x_5, x_1);
-if (x_8 == 0)
-{
-lean_object* x_9; 
-x_9 = l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_1, x_2, x_7);
-lean_ctor_set(x_3, 2, x_9);
-return x_3;
-}
-else
-{
-lean_dec(x_6);
-lean_dec(x_5);
-lean_ctor_set(x_3, 1, x_2);
-lean_ctor_set(x_3, 0, x_1);
-return x_3;
-}
-}
-else
-{
-lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_10 = lean_ctor_get(x_3, 0);
-x_11 = lean_ctor_get(x_3, 1);
-x_12 = lean_ctor_get(x_3, 2);
-lean_inc(x_12);
-lean_inc(x_11);
-lean_inc(x_10);
 lean_dec(x_3);
-x_13 = lean_expr_eqv(x_10, x_1);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; 
-x_14 = l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_1, x_2, x_12);
-x_15 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_15, 0, x_10);
-lean_ctor_set(x_15, 1, x_11);
-lean_ctor_set(x_15, 2, x_14);
-return x_15;
+return x_1;
 }
 else
 {
-lean_object* x_16; 
-lean_dec(x_11);
-lean_dec(x_10);
-x_16 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_16, 0, x_1);
-lean_ctor_set(x_16, 1, x_2);
-lean_ctor_set(x_16, 2, x_12);
-return x_16;
-}
-}
-}
-}
-}
-lean_object* l_HashMapImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
 uint8_t x_4; 
 x_4 = !lean_is_exclusive(x_1);
 if (x_4 == 0)
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; lean_object* x_10; uint8_t x_11; 
+lean_object* x_5; lean_object* x_6; uint8_t x_7; 
 x_5 = lean_ctor_get(x_1, 0);
 x_6 = lean_ctor_get(x_1, 1);
-x_7 = lean_array_get_size(x_6);
-x_8 = l_Lean_Expr_hash(x_2);
-x_9 = lean_usize_modn(x_8, x_7);
-x_10 = lean_array_uget(x_6, x_9);
-x_11 = l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_10);
+x_7 = lean_expr_eqv(x_5, x_2);
+if (x_7 == 0)
+{
+lean_object* x_8; 
+x_8 = l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_6, x_2, x_3);
+lean_ctor_set(x_1, 1, x_8);
+return x_1;
+}
+else
+{
+lean_dec(x_5);
+lean_ctor_set(x_1, 0, x_3);
+return x_1;
+}
+}
+else
+{
+lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_9 = lean_ctor_get(x_1, 0);
+x_10 = lean_ctor_get(x_1, 1);
+lean_inc(x_10);
+lean_inc(x_9);
+lean_dec(x_1);
+x_11 = lean_expr_eqv(x_9, x_2);
 if (x_11 == 0)
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; 
-x_12 = lean_unsigned_to_nat(1u);
-x_13 = lean_nat_add(x_5, x_12);
-lean_dec(x_5);
-x_14 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_14, 0, x_2);
-lean_ctor_set(x_14, 1, x_3);
-lean_ctor_set(x_14, 2, x_10);
-x_15 = lean_array_uset(x_6, x_9, x_14);
-x_16 = lean_nat_dec_le(x_13, x_7);
-lean_dec(x_7);
-if (x_16 == 0)
+lean_object* x_12; lean_object* x_13; 
+x_12 = l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_10, x_2, x_3);
+x_13 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_13, 0, x_9);
+lean_ctor_set(x_13, 1, x_12);
+return x_13;
+}
+else
 {
-lean_object* x_17; 
+lean_object* x_14; 
+lean_dec(x_9);
+x_14 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_14, 0, x_3);
+lean_ctor_set(x_14, 1, x_10);
+return x_14;
+}
+}
+}
+}
+}
+lean_object* l_HashSetImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = !lean_is_exclusive(x_1);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; uint8_t x_10; 
+x_4 = lean_ctor_get(x_1, 0);
+x_5 = lean_ctor_get(x_1, 1);
+x_6 = lean_array_get_size(x_5);
+x_7 = l_Lean_Expr_hash(x_2);
+x_8 = lean_usize_modn(x_7, x_6);
+x_9 = lean_array_uget(x_5, x_8);
+x_10 = l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; 
+x_11 = lean_unsigned_to_nat(1u);
+x_12 = lean_nat_add(x_4, x_11);
+lean_dec(x_4);
+x_13 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_13, 0, x_2);
+lean_ctor_set(x_13, 1, x_9);
+x_14 = lean_array_uset(x_5, x_8, x_13);
+x_15 = lean_nat_dec_le(x_12, x_6);
+lean_dec(x_6);
+if (x_15 == 0)
+{
+lean_object* x_16; 
 lean_free_object(x_1);
-x_17 = l_HashMapImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(x_13, x_15);
-return x_17;
+x_16 = l_HashSetImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(x_12, x_14);
+return x_16;
 }
 else
 {
-lean_ctor_set(x_1, 1, x_15);
-lean_ctor_set(x_1, 0, x_13);
+lean_ctor_set(x_1, 1, x_14);
+lean_ctor_set(x_1, 0, x_12);
 return x_1;
 }
 }
 else
 {
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_7);
-x_18 = l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_2, x_3, x_10);
-x_19 = lean_array_uset(x_6, x_9, x_18);
-lean_ctor_set(x_1, 1, x_19);
+lean_object* x_17; lean_object* x_18; 
+lean_dec(x_6);
+lean_inc(x_2);
+x_17 = l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_9, x_2, x_2);
+lean_dec(x_2);
+x_18 = lean_array_uset(x_5, x_8, x_17);
+lean_ctor_set(x_1, 1, x_18);
 return x_1;
 }
 }
 else
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; size_t x_24; lean_object* x_25; uint8_t x_26; 
-x_20 = lean_ctor_get(x_1, 0);
-x_21 = lean_ctor_get(x_1, 1);
-lean_inc(x_21);
+lean_object* x_19; lean_object* x_20; lean_object* x_21; size_t x_22; size_t x_23; lean_object* x_24; uint8_t x_25; 
+x_19 = lean_ctor_get(x_1, 0);
+x_20 = lean_ctor_get(x_1, 1);
 lean_inc(x_20);
+lean_inc(x_19);
 lean_dec(x_1);
-x_22 = lean_array_get_size(x_21);
-x_23 = l_Lean_Expr_hash(x_2);
-x_24 = lean_usize_modn(x_23, x_22);
-x_25 = lean_array_uget(x_21, x_24);
-x_26 = l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_25);
-if (x_26 == 0)
+x_21 = lean_array_get_size(x_20);
+x_22 = l_Lean_Expr_hash(x_2);
+x_23 = lean_usize_modn(x_22, x_21);
+x_24 = lean_array_uget(x_20, x_23);
+x_25 = l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_2, x_24);
+if (x_25 == 0)
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; 
-x_27 = lean_unsigned_to_nat(1u);
-x_28 = lean_nat_add(x_20, x_27);
-lean_dec(x_20);
-x_29 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_29, 0, x_2);
-lean_ctor_set(x_29, 1, x_3);
-lean_ctor_set(x_29, 2, x_25);
-x_30 = lean_array_uset(x_21, x_24, x_29);
-x_31 = lean_nat_dec_le(x_28, x_22);
-lean_dec(x_22);
-if (x_31 == 0)
+lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; 
+x_26 = lean_unsigned_to_nat(1u);
+x_27 = lean_nat_add(x_19, x_26);
+lean_dec(x_19);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_2);
+lean_ctor_set(x_28, 1, x_24);
+x_29 = lean_array_uset(x_20, x_23, x_28);
+x_30 = lean_nat_dec_le(x_27, x_21);
+lean_dec(x_21);
+if (x_30 == 0)
+{
+lean_object* x_31; 
+x_31 = l_HashSetImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(x_27, x_29);
+return x_31;
+}
+else
 {
 lean_object* x_32; 
-x_32 = l_HashMapImp_expand___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__4(x_28, x_30);
+x_32 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_32, 0, x_27);
+lean_ctor_set(x_32, 1, x_29);
 return x_32;
 }
-else
-{
-lean_object* x_33; 
-x_33 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_33, 0, x_28);
-lean_ctor_set(x_33, 1, x_30);
-return x_33;
-}
 }
 else
 {
-lean_object* x_34; lean_object* x_35; lean_object* x_36; 
-lean_dec(x_22);
-x_34 = l_AssocList_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_2, x_3, x_25);
-x_35 = lean_array_uset(x_21, x_24, x_34);
-x_36 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_36, 0, x_20);
-lean_ctor_set(x_36, 1, x_35);
-return x_36;
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+lean_dec(x_21);
+lean_inc(x_2);
+x_33 = l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_24, x_2, x_2);
+lean_dec(x_2);
+x_34 = lean_array_uset(x_20, x_23, x_33);
+x_35 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_35, 0, x_19);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
@ -14050,91 +14042,111 @@ return x_36;
 lean_object* l___private_Init_Lean_MetavarContext_6__visit_x3f(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; uint8_t x_14; 
-x_14 = l_Lean_Expr_hasMVar(x_1);
-if (x_14 == 0)
-{
-uint8_t x_15; 
-x_15 = l_Lean_Expr_hasFVar(x_1);
-if (x_15 == 0)
-{
-uint8_t x_16; lean_object* x_17; lean_object* x_18; 
-lean_dec(x_1);
-x_16 = 0;
-x_17 = lean_box(x_16);
-x_18 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_18, 0, x_17);
-lean_ctor_set(x_18, 1, x_2);
-return x_18;
-}
-else
-{
-lean_object* x_19; 
-x_19 = lean_box(0);
-x_3 = x_19;
-goto block_13;
-}
-}
-else
-{
-lean_object* x_20; 
-x_20 = lean_box(0);
-x_3 = x_20;
-goto block_13;
-}
-block_13:
+uint8_t x_3; 
+x_3 = l_Lean_Expr_hasMVar(x_1);
+if (x_3 == 0)
 {
 uint8_t x_4; 
-lean_dec(x_3);
-x_4 = l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(x_2, x_1);
+x_4 = l_Lean_Expr_hasFVar(x_1);
 if (x_4 == 0)
 {
-lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; 
-x_5 = lean_box(0);
-x_6 = l_HashMapImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(x_2, x_1, x_5);
-x_7 = 1;
-x_8 = lean_box(x_7);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_8);
-lean_ctor_set(x_9, 1, x_6);
-return x_9;
+uint8_t x_5; lean_object* x_6; lean_object* x_7; 
+lean_dec(x_1);
+x_5 = 0;
+x_6 = lean_box(x_5);
+x_7 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_7, 0, x_6);
+lean_ctor_set(x_7, 1, x_2);
+return x_7;
 }
 else
 {
-uint8_t x_10; lean_object* x_11; lean_object* x_12; 
-lean_dec(x_1);
-x_10 = 0;
+uint8_t x_8; 
+x_8 = l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(x_2, x_1);
+if (x_8 == 0)
+{
+lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; 
+x_9 = l_HashSetImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(x_2, x_1);
+x_10 = 1;
 x_11 = lean_box(x_10);
 x_12 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_2);
+lean_ctor_set(x_12, 1, x_9);
 return x_12;
 }
+else
+{
+uint8_t x_13; lean_object* x_14; lean_object* x_15; 
+lean_dec(x_1);
+x_13 = 0;
+x_14 = lean_box(x_13);
+x_15 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_15, 0, x_14);
+lean_ctor_set(x_15, 1, x_2);
+return x_15;
 }
 }
 }
-lean_object* l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+else
+{
+uint8_t x_16; 
+x_16 = l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(x_2, x_1);
+if (x_16 == 0)
+{
+lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20; 
+x_17 = l_HashSetImp_insert___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__3(x_2, x_1);
+x_18 = 1;
+x_19 = lean_box(x_18);
+x_20 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_20, 0, x_19);
+lean_ctor_set(x_20, 1, x_17);
+return x_20;
+}
+else
+{
+uint8_t x_21; lean_object* x_22; lean_object* x_23; 
+lean_dec(x_1);
+x_21 = 0;
+x_22 = lean_box(x_21);
+x_23 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_23, 0, x_22);
+lean_ctor_set(x_23, 1, x_2);
+return x_23;
+}
+}
+}
+}
+lean_object* l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; 
-x_3 = l_AssocList_contains___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_1, x_2);
+x_3 = l_List_elem___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__2(x_1, x_2);
 lean_dec(x_2);
 lean_dec(x_1);
 x_4 = lean_box(x_3);
 return x_4;
 }
 }
-lean_object* l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; 
-x_3 = l_HashMapImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(x_1, x_2);
+x_3 = l_HashSetImp_contains___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__1(x_1, x_2);
 lean_dec(x_2);
 lean_dec(x_1);
 x_4 = lean_box(x_3);
 return x_4;
 }
 }
+lean_object* l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_List_replace___main___at___private_Init_Lean_MetavarContext_6__visit_x3f___spec__7(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
 lean_object* l___private_Init_Lean_MetavarContext_7__visit(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -15172,19 +15184,11 @@ return x_11;
 }
 }
 }
-lean_object* l_mkHashMap___at_Lean_MetavarContext_findExprDependsOn___spec__2(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_mkHashMapImp___rarg(x_1);
-return x_2;
-}
-}
 lean_object* l_mkHashSet___at_Lean_MetavarContext_findExprDependsOn___spec__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_mkHashMapImp___rarg(x_1);
+x_2 = l_mkHashSetImp___rarg(x_1);
 return x_2;
 }
 }
@ -15193,7 +15197,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = lean_unsigned_to_nat(8u);
-x_2 = l_mkHashMapImp___rarg(x_1);
+x_2 = l_mkHashSetImp___rarg(x_1);
 return x_2;
 }
 }
@ -15266,7 +15270,7 @@ return x_8;
 else
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_9 = l_HashMap_Inhabited___closed__1;
+x_9 = l_HashSet_Inhabited___closed__1;
 x_10 = l___private_Init_Lean_MetavarContext_8__dep___main(x_1, x_3, x_4, x_9);
 x_11 = lean_ctor_get(x_10, 0);
 lean_inc(x_11);
@ -15277,7 +15281,7 @@ return x_11;
 else
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_12 = l_HashMap_Inhabited___closed__1;
+x_12 = l_HashSet_Inhabited___closed__1;
 x_13 = l___private_Init_Lean_MetavarContext_8__dep___main(x_1, x_3, x_4, x_12);
 x_14 = lean_ctor_get(x_13, 0);
 lean_inc(x_14);
@ -15303,7 +15307,7 @@ if (x_30 == 0)
 uint8_t x_31; lean_object* x_32; 
 lean_dec(x_15);
 x_31 = 0;
-x_32 = l_HashMap_Inhabited___closed__1;
+x_32 = l_HashSet_Inhabited___closed__1;
 x_17 = x_31;
 x_18 = x_32;
 goto block_28;
@ -15311,7 +15315,7 @@ goto block_28;
 else
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; 
-x_33 = l_HashMap_Inhabited___closed__1;
+x_33 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_3);
 lean_inc(x_1);
 x_34 = l___private_Init_Lean_MetavarContext_8__dep___main(x_1, x_3, x_15, x_33);
@ -15330,7 +15334,7 @@ goto block_28;
 else
 {
 lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; 
-x_38 = l_HashMap_Inhabited___closed__1;
+x_38 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_3);
 lean_inc(x_1);
 x_39 = l___private_Init_Lean_MetavarContext_8__dep___main(x_1, x_3, x_15, x_38);
@ -17575,7 +17579,7 @@ return x_7;
 else
 {
 lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = l_HashMap_Inhabited___closed__1;
+x_8 = l_HashSet_Inhabited___closed__1;
 x_9 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_exprDependsOn___spec__1(x_3, x_1, x_2, x_8);
 x_10 = lean_ctor_get(x_9, 0);
 lean_inc(x_10);
@ -17586,7 +17590,7 @@ return x_10;
 else
 {
 lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_11 = l_HashMap_Inhabited___closed__1;
+x_11 = l_HashSet_Inhabited___closed__1;
 x_12 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_exprDependsOn___spec__7(x_3, x_1, x_2, x_11);
 x_13 = lean_ctor_get(x_12, 0);
 lean_inc(x_13);
@ -24232,7 +24236,7 @@ return x_8;
 else
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_9 = l_HashMap_Inhabited___closed__1;
+x_9 = l_HashSet_Inhabited___closed__1;
 x_10 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_localDeclDependsOn___spec__1(x_3, x_1, x_4, x_9);
 x_11 = lean_ctor_get(x_10, 0);
 lean_inc(x_11);
@ -24243,7 +24247,7 @@ return x_11;
 else
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_12 = l_HashMap_Inhabited___closed__1;
+x_12 = l_HashSet_Inhabited___closed__1;
 x_13 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_localDeclDependsOn___spec__7(x_3, x_1, x_4, x_12);
 x_14 = lean_ctor_get(x_13, 0);
 lean_inc(x_14);
@ -24269,7 +24273,7 @@ if (x_30 == 0)
 uint8_t x_31; lean_object* x_32; 
 lean_dec(x_15);
 x_31 = 0;
-x_32 = l_HashMap_Inhabited___closed__1;
+x_32 = l_HashSet_Inhabited___closed__1;
 x_17 = x_31;
 x_18 = x_32;
 goto block_28;
@ -24277,7 +24281,7 @@ goto block_28;
 else
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; 
-x_33 = l_HashMap_Inhabited___closed__1;
+x_33 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_34 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_localDeclDependsOn___spec__25(x_3, x_1, x_15, x_33);
 x_35 = lean_ctor_get(x_34, 0);
@ -24295,7 +24299,7 @@ goto block_28;
 else
 {
 lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; 
-x_38 = l_HashMap_Inhabited___closed__1;
+x_38 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_39 = l___private_Init_Lean_MetavarContext_8__dep___main___at_Lean_MetavarContext_localDeclDependsOn___spec__31(x_3, x_1, x_15, x_38);
 x_40 = lean_ctor_get(x_39, 0);
@ -32595,7 +32599,7 @@ return x_25;
 else
 {
 lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; 
-x_26 = l_HashMap_Inhabited___closed__1;
+x_26 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_27 = l___private_Init_Lean_MetavarContext_8__dep___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__4(x_6, x_1, x_22, x_26);
 x_28 = lean_ctor_get(x_27, 0);
@ -32626,7 +32630,7 @@ goto block_18;
 else
 {
 lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35; 
-x_32 = l_HashMap_Inhabited___closed__1;
+x_32 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_33 = l___private_Init_Lean_MetavarContext_8__dep___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__10(x_6, x_1, x_22, x_32);
 x_34 = lean_ctor_get(x_33, 0);
@ -32671,7 +32675,7 @@ if (x_58 == 0)
 uint8_t x_59; lean_object* x_60; 
 lean_dec(x_38);
 x_59 = 0;
-x_60 = l_HashMap_Inhabited___closed__1;
+x_60 = l_HashSet_Inhabited___closed__1;
 x_40 = x_59;
 x_41 = x_60;
 goto block_56;
@ -32679,7 +32683,7 @@ goto block_56;
 else
 {
 lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; uint8_t x_65; 
-x_61 = l_HashMap_Inhabited___closed__1;
+x_61 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_62 = l___private_Init_Lean_MetavarContext_8__dep___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__28(x_6, x_1, x_38, x_61);
 x_63 = lean_ctor_get(x_62, 0);
@ -32697,7 +32701,7 @@ goto block_56;
 else
 {
 lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; uint8_t x_70; 
-x_66 = l_HashMap_Inhabited___closed__1;
+x_66 = l_HashSet_Inhabited___closed__1;
 lean_inc(x_1);
 x_67 = l___private_Init_Lean_MetavarContext_8__dep___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__34(x_6, x_1, x_38, x_66);
 x_68 = lean_ctor_get(x_67, 0);
--- a/stage0/stdlib/Init/Lean/Util/CollectFVars.c
+++ b/stage0/stdlib/Init/Lean/Util/CollectFVars.c
--- a/stage0/stdlib/Init/Lean/Util/CollectLevelParams.c
+++ b/stage0/stdlib/Init/Lean/Util/CollectLevelParams.c
--- a/stage0/stdlib/Init/Lean/Util/CollectMVars.c
+++ b/stage0/stdlib/Init/Lean/Util/CollectMVars.c
--- a/stage0/stdlib/Init/ShareCommon.c
+++ b/stage0/stdlib/Init/ShareCommon.c
@ -14,11 +14,11 @@
 extern "C" {
 #endif
 lean_object* l_PersistentHashMap_findAux___main___at_ShareCommon_ObjectPersistentMap_find_x3f___spec__2(lean_object*, size_t, lean_object*);
-lean_object* l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(lean_object*, lean_object*);
 size_t l_USize_add(size_t, size_t);
 lean_object* l_PersistentHashMap_findEntryAux___main___at_ShareCommon_ObjectPersistentSet_find_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_shareCommon(lean_object*);
 lean_object* l_ShareCommon_mkPersistentState___boxed(lean_object*);
+lean_object* l_mkHashSetImp___rarg(lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentSet___spec__1___closed__3;
 lean_object* l_ShareCommon_PersistentState_shareCommon___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_sharecommon_mk_pstate(lean_object*);
@ -37,6 +37,8 @@ lean_object* lean_object_map_insert(lean_object*, lean_object*, lean_object*);
 size_t l_USize_sub(size_t, size_t);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentSet___spec__1;
 lean_object* l_PShareCommonT_run___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(lean_object*, lean_object*);
+lean_object* l_HashSetImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommon_State_shareCommon___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommon_PersistentState_inhabited;
 lean_object* l_PShareCommonT_withShareCommon(lean_object*);
@ -44,6 +46,7 @@ lean_object* l_shareCommonM(lean_object*, lean_object*);
 lean_object* l_ShareCommonT_monadShareCommon(lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
+lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
 lean_object* l_shareCommon___rarg(lean_object*);
 lean_object* l_ShareCommon_Object_ptrEq___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findEntry_x3f___at_ShareCommon_ObjectPersistentSet_find_x3f___spec__1___boxed(lean_object*, lean_object*);
@ -56,18 +59,17 @@ lean_object* l_PersistentHashMap_findEntryAtAux___main___at_ShareCommon_ObjectPe
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* lean_object_set_insert(lean_object*, lean_object*);
 lean_object* l_ShareCommon_PersistentState_empty___closed__1;
-lean_object* l_HashMapImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommonT_withShareCommon___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PShareCommonT_monadShareCommon___rarg(lean_object*);
 lean_object* l_HashMapImp_expand___at_ShareCommon_ObjectMap_insert___spec__3(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentSet___spec__1___closed__2;
 lean_object* l_Array_iterateMAux___main___at_ShareCommon_ObjectPersistentSet_insert___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
+uint8_t l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2(lean_object*, lean_object*);
 lean_object* l_ShareCommonT_run___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommon_mkObjectSet___closed__1;
 lean_object* l_AssocList_find_x3f___main___at_ShareCommon_ObjectMap_find_x3f___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insert___at_ShareCommon_ObjectPersistentSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_HashMapImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_HashMapImp_moveEntries___main___at_ShareCommon_ObjectMap_insert___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommon_PersistentState_empty;
 lean_object* l_ShareCommon_StatePointed;
@ -76,12 +78,15 @@ lean_object* lean_sharecommon_mk_state(lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_ShareCommon_ObjectPersistentSet_insert___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ShareCommon_Object_eq___boxed(lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
+lean_object* l_List_foldl___main___at_ShareCommon_ObjectSet_insert___spec__5(lean_object*, lean_object*);
 lean_object* lean_mk_object_map(lean_object*);
 lean_object* l_ShareCommonT_withShareCommon___at_shareCommon___spec__1(lean_object*);
 lean_object* lean_persistent_state_sharecommon(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_ShareCommon_ObjectPersistentMap_find_x3f___spec__1(lean_object*, lean_object*);
+lean_object* l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_object_pmap(lean_object*);
 extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
+lean_object* l_HashSetImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(lean_object*, lean_object*);
 lean_object* l_AssocList_replace___main___at_ShareCommon_ObjectMap_insert___spec__6(lean_object*, lean_object*, lean_object*);
 size_t lean_usize_modn(size_t, lean_object*);
 lean_object* l_PShareCommonT_monadShareCommon(lean_object*);
@ -92,7 +97,6 @@ size_t l_USize_mul(size_t, size_t);
 lean_object* l_mkHashMapImp___rarg(lean_object*);
 lean_object* lean_object_pset_insert(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findEntry_x3f___at_ShareCommon_ObjectPersistentSet_find_x3f___spec__1(lean_object*, lean_object*);
-lean_object* l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(lean_object*, lean_object*, lean_object*);
 lean_object* l_PShareCommonT_run(lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_ShareCommon_ObjectPersistentMap_find_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentSet___spec__1___closed__1;
@ -104,6 +108,7 @@ lean_object* l_ShareCommonT_monadShareCommon___rarg(lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentMap___spec__1;
 lean_object* l_ShareCommonT_withShareCommon___at_shareCommon___spec__1___rarg(lean_object*, lean_object*);
 lean_object* l_ShareCommonT_withShareCommon(lean_object*);
+lean_object* l_HashSetImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(lean_object*, lean_object*);
 size_t lean_ptr_addr(lean_object*);
 lean_object* lean_object_set_find(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_ShareCommon_ObjectPersistentSet_insert___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -116,34 +121,29 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t l_USize_decLe(size_t, size_t);
 lean_object* l_mkHashSet___at_ShareCommon_mkObjectSet___spec__1(lean_object*);
 lean_object* l_PersistentHashMap_findEntryAtAux___main___at_ShareCommon_ObjectPersistentSet_find_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_HashMapImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(lean_object*, lean_object*);
 lean_object* l_AssocList_foldlM___main___at_ShareCommon_ObjectMap_insert___spec__5(lean_object*, lean_object*);
-lean_object* l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1___boxed(lean_object*, lean_object*);
 uint8_t l_AssocList_contains___main___at_ShareCommon_ObjectMap_insert___spec__2(lean_object*, lean_object*);
-lean_object* l_AssocList_foldlM___main___at_ShareCommon_ObjectSet_insert___spec__5(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_ShareCommon_ObjectPersistentMap_insert___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
 lean_object* l_AssocList_contains___main___at_ShareCommon_ObjectMap_insert___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAtAux___main___at_ShareCommon_ObjectPersistentMap_find_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_HashMapImp_find_x3f___at_ShareCommon_ObjectMap_find_x3f___spec__1(lean_object*, lean_object*);
 lean_object* lean_nat_mul(lean_object*, lean_object*);
-lean_object* l_mkHashMap___at_ShareCommon_mkObjectSet___spec__2(lean_object*);
 uint8_t lean_sharecommon_eq(lean_object*, lean_object*);
-lean_object* l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
+lean_object* l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1___boxed(lean_object*, lean_object*);
+lean_object* l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2___boxed(lean_object*, lean_object*);
 size_t lean_sharecommon_hash(lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentMap___spec__1___closed__2;
 lean_object* l_ShareCommon_Object_hash___boxed(lean_object*);
-lean_object* l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at_ShareCommon_ObjectPersistentSet_insert___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentMap___spec__1___closed__1;
 lean_object* l_ShareCommon_State_empty;
 lean_object* l_HashMapImp_insert___at_ShareCommon_ObjectMap_insert___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentMap___spec__1___closed__3;
-lean_object* l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2(lean_object*, lean_object*);
+lean_object* l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_ShareCommon_ObjectPersistentMap_insert___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_object_map_find(lean_object*, lean_object*);
-uint8_t l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2(lean_object*, lean_object*);
 lean_object* lean_usize_to_nat(size_t);
 lean_object* lean_state_sharecommon(lean_object*, lean_object*);
 lean_object* lean_object_pset_find(lean_object*, lean_object*);
@ -665,19 +665,11 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
-lean_object* l_mkHashMap___at_ShareCommon_mkObjectSet___spec__2(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_mkHashMapImp___rarg(x_1);
-return x_2;
-}
-}
 lean_object* l_mkHashSet___at_ShareCommon_mkObjectSet___spec__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = l_mkHashMapImp___rarg(x_1);
+x_2 = l_mkHashSetImp___rarg(x_1);
 return x_2;
 }
 }
@ -686,7 +678,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = lean_unsigned_to_nat(1024u);
-x_2 = l_mkHashMapImp___rarg(x_1);
+x_2 = l_mkHashSetImp___rarg(x_1);
 return x_2;
 }
 }
@ -699,121 +691,41 @@ x_2 = l_ShareCommon_mkObjectSet___closed__1;
 return x_2;
 }
 }
-lean_object* l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2(lean_object* x_1, lean_object* x_2) {
+lean_object* l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-if (lean_obj_tag(x_2) == 0)
-{
-lean_object* x_3; 
-x_3 = lean_box(0);
-return x_3;
-}
-else
-{
-lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; 
-x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 1);
-x_6 = lean_ctor_get(x_2, 2);
-x_7 = lean_sharecommon_eq(x_4, x_1);
-if (x_7 == 0)
-{
-x_2 = x_6;
-goto _start;
-}
-else
-{
-lean_object* x_9; lean_object* x_10; 
-lean_inc(x_5);
-lean_inc(x_4);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_4);
-lean_ctor_set(x_9, 1, x_5);
-x_10 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_10, 0, x_9);
-return x_10;
-}
-}
-}
-}
-lean_object* l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_8; 
+lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
 x_3 = lean_ctor_get(x_1, 1);
 x_4 = lean_array_get_size(x_3);
 x_5 = lean_sharecommon_hash(x_2);
 x_6 = lean_usize_modn(x_5, x_4);
 lean_dec(x_4);
-x_7 = lean_array_uget(x_3, x_6);
-x_8 = l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2(x_2, x_7);
-lean_dec(x_7);
-return x_8;
+x_7 = lean_alloc_closure((void*)(l_ShareCommon_Object_eq___boxed), 2, 1);
+lean_closure_set(x_7, 0, x_2);
+x_8 = lean_array_uget(x_3, x_6);
+x_9 = l_List_find_x3f___main___rarg(x_7, x_8);
+return x_9;
 }
 }
 lean_object* lean_object_set_find(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(x_1, x_2);
-lean_dec(x_2);
+x_3 = l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(x_1, x_2);
 lean_dec(x_1);
-if (lean_obj_tag(x_3) == 0)
-{
-lean_object* x_4; 
-x_4 = lean_box(0);
-return x_4;
-}
-else
-{
-uint8_t x_5; 
-x_5 = !lean_is_exclusive(x_3);
-if (x_5 == 0)
-{
-lean_object* x_6; lean_object* x_7; 
-x_6 = lean_ctor_get(x_3, 0);
-x_7 = lean_ctor_get(x_6, 0);
-lean_inc(x_7);
-lean_dec(x_6);
-lean_ctor_set(x_3, 0, x_7);
 return x_3;
 }
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_3, 0);
-lean_inc(x_8);
-lean_dec(x_3);
-x_9 = lean_ctor_get(x_8, 0);
-lean_inc(x_9);
-lean_dec(x_8);
-x_10 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_10, 0, x_9);
-return x_10;
 }
-}
-}
-}
-lean_object* l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_AssocList_findEntry_x3f___main___at_ShareCommon_ObjectSet_find_x3f___spec__2(x_1, x_2);
-lean_dec(x_2);
+x_3 = l_HashSetImp_find_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(x_1, x_2);
 lean_dec(x_1);
 return x_3;
 }
 }
-lean_object* l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = l_HashMapImp_findEntry_x3f___at_ShareCommon_ObjectSet_find_x3f___spec__1(x_1, x_2);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_3;
-}
-}
-uint8_t l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2(lean_object* x_1, lean_object* x_2) {
+uint8_t l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
@ -826,8 +738,8 @@ else
 {
 lean_object* x_4; lean_object* x_5; uint8_t x_6; 
 x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 2);
-x_6 = lean_sharecommon_eq(x_4, x_1);
+x_5 = lean_ctor_get(x_2, 1);
+x_6 = lean_sharecommon_eq(x_1, x_4);
 if (x_6 == 0)
 {
 x_2 = x_5;
@ -842,7 +754,7 @@ return x_8;
 }
 }
 }
-lean_object* l_AssocList_foldlM___main___at_ShareCommon_ObjectSet_insert___spec__5(lean_object* x_1, lean_object* x_2) {
+lean_object* l_List_foldl___main___at_ShareCommon_ObjectSet_insert___spec__5(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_2) == 0)
@ -857,13 +769,13 @@ if (x_3 == 0)
 {
 lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; 
 x_4 = lean_ctor_get(x_2, 0);
-x_5 = lean_ctor_get(x_2, 2);
+x_5 = lean_ctor_get(x_2, 1);
 x_6 = lean_array_get_size(x_1);
 x_7 = lean_sharecommon_hash(x_4);
 x_8 = lean_usize_modn(x_7, x_6);
 lean_dec(x_6);
 x_9 = lean_array_uget(x_1, x_8);
-lean_ctor_set(x_2, 2, x_9);
+lean_ctor_set(x_2, 1, x_9);
 x_10 = lean_array_uset(x_1, x_8, x_2);
 x_1 = x_10;
 x_2 = x_5;
@ -871,32 +783,29 @@ goto _start;
 }
 else
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
 x_12 = lean_ctor_get(x_2, 0);
 x_13 = lean_ctor_get(x_2, 1);
-x_14 = lean_ctor_get(x_2, 2);
-lean_inc(x_14);
 lean_inc(x_13);
 lean_inc(x_12);
 lean_dec(x_2);
-x_15 = lean_array_get_size(x_1);
-x_16 = lean_sharecommon_hash(x_12);
-x_17 = lean_usize_modn(x_16, x_15);
-lean_dec(x_15);
-x_18 = lean_array_uget(x_1, x_17);
-x_19 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_19, 0, x_12);
-lean_ctor_set(x_19, 1, x_13);
-lean_ctor_set(x_19, 2, x_18);
-x_20 = lean_array_uset(x_1, x_17, x_19);
-x_1 = x_20;
-x_2 = x_14;
+x_14 = lean_array_get_size(x_1);
+x_15 = lean_sharecommon_hash(x_12);
+x_16 = lean_usize_modn(x_15, x_14);
+lean_dec(x_14);
+x_17 = lean_array_uget(x_1, x_16);
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_12);
+lean_ctor_set(x_18, 1, x_17);
+x_19 = lean_array_uset(x_1, x_16, x_18);
+x_1 = x_19;
+x_2 = x_13;
 goto _start;
 }
 }
 }
 }
-lean_object* l_HashMapImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_HashSetImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -915,7 +824,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_obj
 x_6 = lean_array_fget(x_2, x_1);
 x_7 = lean_box(0);
 x_8 = lean_array_fset(x_2, x_1, x_7);
-x_9 = l_AssocList_foldlM___main___at_ShareCommon_ObjectSet_insert___spec__5(x_3, x_6);
+x_9 = l_List_foldl___main___at_ShareCommon_ObjectSet_insert___spec__5(x_3, x_6);
 x_10 = lean_unsigned_to_nat(1u);
 x_11 = lean_nat_add(x_1, x_10);
 lean_dec(x_1);
@ -926,7 +835,7 @@ goto _start;
 }
 }
 }
-lean_object* l_HashMapImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(lean_object* x_1, lean_object* x_2) {
+lean_object* l_HashSetImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
@ -937,188 +846,181 @@ lean_dec(x_3);
 x_6 = lean_box(0);
 x_7 = lean_mk_array(x_5, x_6);
 x_8 = lean_unsigned_to_nat(0u);
-x_9 = l_HashMapImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(x_8, x_2, x_7);
+x_9 = l_HashSetImp_moveEntries___main___at_ShareCommon_ObjectSet_insert___spec__4(x_8, x_2, x_7);
 x_10 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_10, 0, x_1);
 lean_ctor_set(x_10, 1, x_9);
 return x_10;
 }
 }
-lean_object* l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-if (lean_obj_tag(x_3) == 0)
+if (lean_obj_tag(x_1) == 0)
 {
-lean_dec(x_2);
-lean_dec(x_1);
-return x_3;
-}
-else
-{
-uint8_t x_4; 
-x_4 = !lean_is_exclusive(x_3);
-if (x_4 == 0)
-{
-lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; 
-x_5 = lean_ctor_get(x_3, 0);
-x_6 = lean_ctor_get(x_3, 1);
-x_7 = lean_ctor_get(x_3, 2);
-x_8 = lean_sharecommon_eq(x_5, x_1);
-if (x_8 == 0)
-{
-lean_object* x_9; 
-x_9 = l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_1, x_2, x_7);
-lean_ctor_set(x_3, 2, x_9);
-return x_3;
-}
-else
-{
-lean_dec(x_6);
-lean_dec(x_5);
-lean_ctor_set(x_3, 1, x_2);
-lean_ctor_set(x_3, 0, x_1);
-return x_3;
-}
-}
-else
-{
-lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
-x_10 = lean_ctor_get(x_3, 0);
-x_11 = lean_ctor_get(x_3, 1);
-x_12 = lean_ctor_get(x_3, 2);
-lean_inc(x_12);
-lean_inc(x_11);
-lean_inc(x_10);
 lean_dec(x_3);
-x_13 = lean_sharecommon_eq(x_10, x_1);
-if (x_13 == 0)
-{
-lean_object* x_14; lean_object* x_15; 
-x_14 = l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_1, x_2, x_12);
-x_15 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_15, 0, x_10);
-lean_ctor_set(x_15, 1, x_11);
-lean_ctor_set(x_15, 2, x_14);
-return x_15;
+return x_1;
 }
 else
 {
-lean_object* x_16; 
-lean_dec(x_11);
-lean_dec(x_10);
-x_16 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_16, 0, x_1);
-lean_ctor_set(x_16, 1, x_2);
-lean_ctor_set(x_16, 2, x_12);
-return x_16;
-}
-}
-}
-}
-}
-lean_object* l_HashMapImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
 uint8_t x_4; 
 x_4 = !lean_is_exclusive(x_1);
 if (x_4 == 0)
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; lean_object* x_10; uint8_t x_11; 
+lean_object* x_5; lean_object* x_6; uint8_t x_7; 
 x_5 = lean_ctor_get(x_1, 0);
 x_6 = lean_ctor_get(x_1, 1);
-x_7 = lean_array_get_size(x_6);
-x_8 = lean_sharecommon_hash(x_2);
-x_9 = lean_usize_modn(x_8, x_7);
-x_10 = lean_array_uget(x_6, x_9);
-x_11 = l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2(x_2, x_10);
+x_7 = lean_sharecommon_eq(x_5, x_2);
+if (x_7 == 0)
+{
+lean_object* x_8; 
+x_8 = l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_6, x_2, x_3);
+lean_ctor_set(x_1, 1, x_8);
+return x_1;
+}
+else
+{
+lean_dec(x_5);
+lean_ctor_set(x_1, 0, x_3);
+return x_1;
+}
+}
+else
+{
+lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_9 = lean_ctor_get(x_1, 0);
+x_10 = lean_ctor_get(x_1, 1);
+lean_inc(x_10);
+lean_inc(x_9);
+lean_dec(x_1);
+x_11 = lean_sharecommon_eq(x_9, x_2);
 if (x_11 == 0)
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; 
-x_12 = lean_unsigned_to_nat(1u);
-x_13 = lean_nat_add(x_5, x_12);
-lean_dec(x_5);
-x_14 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_14, 0, x_2);
-lean_ctor_set(x_14, 1, x_3);
-lean_ctor_set(x_14, 2, x_10);
-x_15 = lean_array_uset(x_6, x_9, x_14);
-x_16 = lean_nat_dec_le(x_13, x_7);
-lean_dec(x_7);
-if (x_16 == 0)
+lean_object* x_12; lean_object* x_13; 
+x_12 = l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_10, x_2, x_3);
+x_13 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_13, 0, x_9);
+lean_ctor_set(x_13, 1, x_12);
+return x_13;
+}
+else
 {
-lean_object* x_17; 
+lean_object* x_14; 
+lean_dec(x_9);
+x_14 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_14, 0, x_3);
+lean_ctor_set(x_14, 1, x_10);
+return x_14;
+}
+}
+}
+}
+}
+lean_object* l_HashSetImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; 
+x_3 = !lean_is_exclusive(x_1);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; uint8_t x_10; 
+x_4 = lean_ctor_get(x_1, 0);
+x_5 = lean_ctor_get(x_1, 1);
+x_6 = lean_array_get_size(x_5);
+x_7 = lean_sharecommon_hash(x_2);
+x_8 = lean_usize_modn(x_7, x_6);
+x_9 = lean_array_uget(x_5, x_8);
+x_10 = l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2(x_2, x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; 
+x_11 = lean_unsigned_to_nat(1u);
+x_12 = lean_nat_add(x_4, x_11);
+lean_dec(x_4);
+x_13 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_13, 0, x_2);
+lean_ctor_set(x_13, 1, x_9);
+x_14 = lean_array_uset(x_5, x_8, x_13);
+x_15 = lean_nat_dec_le(x_12, x_6);
+lean_dec(x_6);
+if (x_15 == 0)
+{
+lean_object* x_16; 
 lean_free_object(x_1);
-x_17 = l_HashMapImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(x_13, x_15);
-return x_17;
+x_16 = l_HashSetImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(x_12, x_14);
+return x_16;
 }
 else
 {
-lean_ctor_set(x_1, 1, x_15);
-lean_ctor_set(x_1, 0, x_13);
+lean_ctor_set(x_1, 1, x_14);
+lean_ctor_set(x_1, 0, x_12);
 return x_1;
 }
 }
 else
 {
-lean_object* x_18; lean_object* x_19; 
-lean_dec(x_7);
-x_18 = l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_2, x_3, x_10);
-x_19 = lean_array_uset(x_6, x_9, x_18);
-lean_ctor_set(x_1, 1, x_19);
+lean_object* x_17; lean_object* x_18; 
+lean_dec(x_6);
+lean_inc(x_2);
+x_17 = l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_9, x_2, x_2);
+lean_dec(x_2);
+x_18 = lean_array_uset(x_5, x_8, x_17);
+lean_ctor_set(x_1, 1, x_18);
 return x_1;
 }
 }
 else
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; size_t x_24; lean_object* x_25; uint8_t x_26; 
-x_20 = lean_ctor_get(x_1, 0);
-x_21 = lean_ctor_get(x_1, 1);
-lean_inc(x_21);
+lean_object* x_19; lean_object* x_20; lean_object* x_21; size_t x_22; size_t x_23; lean_object* x_24; uint8_t x_25; 
+x_19 = lean_ctor_get(x_1, 0);
+x_20 = lean_ctor_get(x_1, 1);
 lean_inc(x_20);
+lean_inc(x_19);
 lean_dec(x_1);
-x_22 = lean_array_get_size(x_21);
-x_23 = lean_sharecommon_hash(x_2);
-x_24 = lean_usize_modn(x_23, x_22);
-x_25 = lean_array_uget(x_21, x_24);
-x_26 = l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2(x_2, x_25);
-if (x_26 == 0)
+x_21 = lean_array_get_size(x_20);
+x_22 = lean_sharecommon_hash(x_2);
+x_23 = lean_usize_modn(x_22, x_21);
+x_24 = lean_array_uget(x_20, x_23);
+x_25 = l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2(x_2, x_24);
+if (x_25 == 0)
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; 
-x_27 = lean_unsigned_to_nat(1u);
-x_28 = lean_nat_add(x_20, x_27);
-lean_dec(x_20);
-x_29 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_29, 0, x_2);
-lean_ctor_set(x_29, 1, x_3);
-lean_ctor_set(x_29, 2, x_25);
-x_30 = lean_array_uset(x_21, x_24, x_29);
-x_31 = lean_nat_dec_le(x_28, x_22);
-lean_dec(x_22);
-if (x_31 == 0)
+lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; 
+x_26 = lean_unsigned_to_nat(1u);
+x_27 = lean_nat_add(x_19, x_26);
+lean_dec(x_19);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_2);
+lean_ctor_set(x_28, 1, x_24);
+x_29 = lean_array_uset(x_20, x_23, x_28);
+x_30 = lean_nat_dec_le(x_27, x_21);
+lean_dec(x_21);
+if (x_30 == 0)
+{
+lean_object* x_31; 
+x_31 = l_HashSetImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(x_27, x_29);
+return x_31;
+}
+else
 {
 lean_object* x_32; 
-x_32 = l_HashMapImp_expand___at_ShareCommon_ObjectSet_insert___spec__3(x_28, x_30);
+x_32 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_32, 0, x_27);
+lean_ctor_set(x_32, 1, x_29);
 return x_32;
 }
-else
-{
-lean_object* x_33; 
-x_33 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_33, 0, x_28);
-lean_ctor_set(x_33, 1, x_30);
-return x_33;
-}
 }
 else
 {
-lean_object* x_34; lean_object* x_35; lean_object* x_36; 
-lean_dec(x_22);
-x_34 = l_AssocList_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_2, x_3, x_25);
-x_35 = lean_array_uset(x_21, x_24, x_34);
-x_36 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_36, 0, x_20);
-lean_ctor_set(x_36, 1, x_35);
-return x_36;
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+lean_dec(x_21);
+lean_inc(x_2);
+x_33 = l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_24, x_2, x_2);
+lean_dec(x_2);
+x_34 = lean_array_uset(x_20, x_23, x_33);
+x_35 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_35, 0, x_19);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
@ -1126,23 +1028,31 @@ return x_36;
 lean_object* lean_object_set_insert(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; 
-x_3 = lean_box(0);
-x_4 = l_HashMapImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(x_1, x_2, x_3);
-return x_4;
+lean_object* x_3; 
+x_3 = l_HashSetImp_insert___at_ShareCommon_ObjectSet_insert___spec__1(x_1, x_2);
+return x_3;
 }
 }
-lean_object* l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; 
-x_3 = l_AssocList_contains___main___at_ShareCommon_ObjectSet_insert___spec__2(x_1, x_2);
+x_3 = l_List_elem___main___at_ShareCommon_ObjectSet_insert___spec__2(x_1, x_2);
 lean_dec(x_2);
 lean_dec(x_1);
 x_4 = lean_box(x_3);
 return x_4;
 }
 }
+lean_object* l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_List_replace___main___at_ShareCommon_ObjectSet_insert___spec__6(x_1, x_2, x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
 lean_object* _init_l_PersistentHashMap_empty___at_ShareCommon_mkObjectPersistentMap___spec__1___closed__1() {
 _start:
 {
--- a/stage0/stdlib/Init/Util.c
+++ b/stage0/stdlib/Init/Util.c
@ -25,12 +25,17 @@ lean_object* l_withPtrEq___rarg(lean_object*, lean_object*);
 lean_object* l_withPtrEqUnsafe(lean_object*);
 lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_dbg_trace(lean_object*, lean_object*);
+lean_object* l_withPtrEqResult(lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_withPtrEqDecEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_withPtrEq___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_unreachable_x21___rarg___closed__2;
+lean_object* l_withPtrEqResult___rarg___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_withPtrEqResultUnsafe(lean_object*, lean_object*, lean_object*);
 lean_object* l_withPtrEqDecEq(lean_object*);
+lean_object* l_withPtrEqResultUnsafe___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_panicWithPos___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_withPtrEqResultUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_dbg_sleep(uint32_t, lean_object*);
 lean_object* l_Nat_repr(lean_object*);
 lean_object* l_withPtrAddr___boxed(lean_object*, lean_object*, lean_object*);
@ -51,6 +56,7 @@ lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
 lean_object* l_unreachable_x21___rarg___closed__1;
 lean_object* l_withPtrAddr___rarg___boxed__const__1;
 lean_object* l_withPtrAddr___rarg(lean_object*, lean_object*);
+lean_object* l_withPtrEqResult___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Util_1__mkPanicMessage___closed__3;
 lean_object* l_dbgSleep___boxed(lean_object*, lean_object*, lean_object*);
@ -306,6 +312,47 @@ lean_dec(x_1);
 return x_5;
 }
 }
+lean_object* l_withPtrEqResultUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+size_t x_4; size_t x_5; uint8_t x_6; 
+x_4 = lean_ptr_addr(x_1);
+x_5 = lean_ptr_addr(x_2);
+x_6 = x_4 == x_5;
+if (x_6 == 0)
+{
+lean_object* x_7; lean_object* x_8; 
+x_7 = lean_box(0);
+x_8 = lean_apply_1(x_3, x_7);
+return x_8;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; 
+x_9 = lean_box(1);
+x_10 = lean_apply_1(x_3, x_9);
+return x_10;
+}
+}
+}
+lean_object* l_withPtrEqResultUnsafe(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_withPtrEqResultUnsafe___rarg___boxed), 3, 0);
+return x_4;
+}
+}
+lean_object* l_withPtrEqResultUnsafe___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_withPtrEqResultUnsafe___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* l_withPtrEq___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@ -375,6 +422,33 @@ lean_dec(x_1);
 return x_4;
 }
 }
+lean_object* l_withPtrEqResult___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+}
+lean_object* l_withPtrEqResult(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_withPtrEqResult___rarg___boxed), 3, 0);
+return x_4;
+}
+}
+lean_object* l_withPtrEqResult___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_withPtrEqResult___rarg(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
 lean_object* _init_l_withPtrAddr___rarg___boxed__const__1() {
 _start:
 {