From c3e9ac73e2b20b4e429b2501e2fa629458976b05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Nov 2019 14:42:42 -0800
Subject: [PATCH] refactor: `default` ==> `arbitrary`

Make sure it is opaque, and avoid `irreducible`
---
 library/Init/Control/EState.lean              |  2 +-
 library/Init/Control/Except.lean              |  2 +-
 library/Init/Control/Monad.lean               |  2 +-
 library/Init/Core.lean                        | 19 ++++----
 library/Init/Data/Array/Basic.lean            |  2 +-
 library/Init/Data/BinomialHeap/Basic.lean     |  4 +-
 library/Init/Data/Hashable.lean               |  4 +-
 library/Init/Data/PersistentArray/Basic.lean  |  2 +-
 library/Init/Data/Random.lean                 |  2 +-
 library/Init/Data/String/Basic.lean           |  2 +-
 library/Init/Data/UInt.lean                   |  4 +-
 library/Init/Fix.lean                         | 14 +++---
 library/Init/Lean/AbstractMetavarContext.lean |  2 +-
 library/Init/Lean/Attributes.lean             | 16 +++----
 library/Init/Lean/AuxRecursor.lean            |  4 +-
 library/Init/Lean/Class.lean                  |  2 +-
 .../Init/Lean/Compiler/ClosedTermCache.lean   |  2 +-
 library/Init/Lean/Compiler/ExportAttr.lean    |  2 +-
 library/Init/Lean/Compiler/ExternAttr.lean    |  4 +-
 library/Init/Lean/Compiler/IR/Basic.lean      |  6 +--
 library/Init/Lean/Compiler/IR/Borrow.lean     |  2 +-
 library/Init/Lean/Compiler/IR/Boxing.lean     | 10 ++---
 library/Init/Lean/Compiler/IR/CompilerM.lean  |  2 +-
 library/Init/Lean/Compiler/IR/CtorLayout.lean |  2 +-
 .../Lean/Compiler/IR/ElimDeadBranches.lean    |  2 +-
 library/Init/Lean/Compiler/IR/EmitC.lean      |  2 +-
 library/Init/Lean/Compiler/IR/RC.lean         |  2 +-
 .../Init/Lean/Compiler/IR/UnboxResult.lean    |  2 +-
 .../Init/Lean/Compiler/ImplementedByAttr.lean |  2 +-
 library/Init/Lean/Compiler/InitAttr.lean      |  2 +-
 library/Init/Lean/Compiler/InlineAttrs.lean   |  2 +-
 .../Init/Lean/Compiler/NeverExtractAttr.lean  |  2 +-
 library/Init/Lean/Compiler/Specialize.lean    |  4 +-
 library/Init/Lean/Declaration.lean            |  4 +-
 library/Init/Lean/Elaborator/Alias.lean       |  2 +-
 library/Init/Lean/Elaborator/Basic.lean       | 18 ++++----
 .../Lean/Elaborator/ElabStrategyAttrs.lean    |  2 +-
 library/Init/Lean/Elaborator/PreTerm.lean     |  4 +-
 library/Init/Lean/Environment.lean            | 44 +++++++++----------
 .../Init/Lean/EqnCompiler/MatchPattern.lean   |  2 +-
 library/Init/Lean/Expr.lean                   | 36 +++++++--------
 library/Init/Lean/Level.lean                  |  4 +-
 library/Init/Lean/LocalContext.lean           |  2 +-
 library/Init/Lean/Message.lean                |  4 +-
 library/Init/Lean/Modifiers.lean              |  4 +-
 library/Init/Lean/Name.lean                   |  2 +-
 library/Init/Lean/Options.lean                |  2 +-
 library/Init/Lean/Parser/Command.lean         |  4 +-
 library/Init/Lean/Parser/Level.lean           |  4 +-
 library/Init/Lean/Parser/Parser.lean          | 14 +++---
 library/Init/Lean/Parser/Term.lean            |  4 +-
 library/Init/Lean/Path.lean                   |  2 +-
 library/Init/Lean/ProjFns.lean                |  8 ++--
 library/Init/Lean/ReducibilityAttrs.lean      |  2 +-
 library/Init/Lean/Runtime.lean                |  4 +-
 library/Init/Lean/Scopes.lean                 |  2 +-
 library/Init/Lean/TypeClass/Synth.lean        | 10 ++---
 library/Init/System/IO.lean                   | 44 +++++++++----------
 library/Init/System/Platform.lean             |  6 +--
 library/Init/Util.lean                        |  4 +-
 60 files changed, 184 insertions(+), 187 deletions(-)

diff --git a/library/Init/Control/EState.lean b/library/Init/Control/EState.lean
index 2b8dc0b13b..bbf958d614 100644
--- a/library/Init/Control/EState.lean
+++ b/library/Init/Control/EState.lean
@@ -36,7 +36,7 @@ namespace EStateM
 variables {ε σ α β : Type u}
 
 instance [Inhabited ε] : Inhabited (EStateM ε σ α) :=
-⟨fun s => Result.error (default ε) s⟩
+⟨fun s => Result.error (arbitrary ε) s⟩
 
 @[inline] protected def pure (a : α) : EStateM ε σ α :=
 fun s => Result.ok a s
diff --git a/library/Init/Control/Except.lean b/library/Init/Control/Except.lean
index fd16f37585..d74d92ca43 100644
--- a/library/Init/Control/Except.lean
+++ b/library/Init/Control/Except.lean
@@ -19,7 +19,7 @@ inductive Except (ε : Type u) (α : Type v)
 attribute [unbox] Except
 
 instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) :=
-⟨Except.error (default ε)⟩
+⟨Except.error (arbitrary ε)⟩
 
 section
 variables {ε : Type u} {α : Type v}
diff --git a/library/Init/Control/Monad.lean b/library/Init/Control/Monad.lean
index 8878ff9d0f..207aae2137 100644
--- a/library/Init/Control/Monad.lean
+++ b/library/Init/Control/Monad.lean
@@ -31,7 +31,7 @@ instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhab
 ⟨pure⟩
 
 instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
-⟨pure $ default _⟩
+⟨pure $ arbitrary _⟩
 
 def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
 bind a id
diff --git a/library/Init/Core.lean b/library/Init/Core.lean
index 24c86abfc2..f1fcf4d048 100644
--- a/library/Init/Core.lean
+++ b/library/Init/Core.lean
@@ -1020,12 +1020,9 @@ structure PointedType :=
 class Inhabited (α : Sort u) :=
 (default : α)
 
-constant default (α : Sort u) [Inhabited α] : α :=
+constant arbitrary (α : Sort u) [Inhabited α] : α :=
 Inhabited.default α
 
-@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
-default α
-
 instance Prop.Inhabited : Inhabited Prop :=
 ⟨True⟩
 
@@ -1033,7 +1030,7 @@ instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabite
 Inhabited.casesOn h (fun b => ⟨fun a => b⟩)
 
 instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀ x, Inhabited (β x)] : Inhabited (∀ x, β x) :=
-⟨fun a => default (β a)⟩
+⟨fun a => arbitrary (β a)⟩
 
 instance : Inhabited Bool := ⟨false⟩
 
@@ -1041,7 +1038,7 @@ instance : Inhabited True := ⟨trivial⟩
 
 instance : Inhabited Nat := ⟨0⟩
 
-instance : Inhabited NonScalar := ⟨⟨default _⟩⟩
+instance : Inhabited NonScalar := ⟨⟨arbitrary _⟩⟩
 
 instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
 
@@ -1052,7 +1049,7 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂
 Nonempty.rec h₂ h₁
 
 instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
-⟨default α⟩
+⟨arbitrary α⟩
 
 theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
 | ⟨w, h⟩ => ⟨w⟩
@@ -1195,10 +1192,10 @@ section
 variables {α : Type u} {β : Type v}
 
 instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) :=
-⟨Sum.inl (default α)⟩
+⟨Sum.inl (arbitrary α)⟩
 
 instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
-⟨Sum.inr (default β)⟩
+⟨Sum.inr (arbitrary β)⟩
 
 instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
 {decEq := fun a b =>
@@ -1219,7 +1216,7 @@ section
 variables {α : Type u} {β : Type v}
 
 instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
-⟨(default α, default β)⟩
+⟨(arbitrary α, arbitrary β)⟩
 
 instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
 {decEq := fun ⟨a, b⟩ ⟨a', b'⟩ =>
@@ -1710,7 +1707,7 @@ noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
 
 noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
 match (propDecidable (Nonempty α)) with
-| (isTrue hp)  => PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
+| (isTrue hp)  => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp))
 | (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)
 
 noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
diff --git a/library/Init/Data/Array/Basic.lean b/library/Init/Data/Array/Basic.lean
index 5d3f2747bc..6d4bd6bb4d 100644
--- a/library/Init/Data/Array/Basic.lean
+++ b/library/Init/Data/Array/Basic.lean
@@ -82,7 +82,7 @@ a.get ⟨i.toNat, h⟩
 /- "Comfortable" version of `fget`. It performs a bound check at runtime. -/
 @[extern "lean_array_get"]
 def get! [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-if h : i < a.size then a.get ⟨i, h⟩ else default α
+if h : i < a.size then a.get ⟨i, h⟩ else arbitrary α
 
 def back [Inhabited α] (a : Array α) : α :=
 a.get! (a.size - 1)
diff --git a/library/Init/Data/BinomialHeap/Basic.lean b/library/Init/Data/BinomialHeap/Basic.lean
index e71db56649..122ab24823 100644
--- a/library/Init/Data/BinomialHeap/Basic.lean
+++ b/library/Init/Data/BinomialHeap/Basic.lean
@@ -68,8 +68,8 @@ else
 
 /- O(log n) -/
 @[specialize] def head [Inhabited α] (lt : α → α → Bool) : Heap α → α
-| Heap.empty        => default α
-| Heap.heap []      => default α
+| Heap.empty        => arbitrary α
+| Heap.heap []      => arbitrary α
 | Heap.heap (h::hs) => hs.foldl (fun r n => if lt r n.val then r else n.val) h.val
 
 @[specialize] def findMin (lt : α → α → Bool) : List (HeapNode α) → Nat → HeapNode α × Nat → HeapNode α × Nat
diff --git a/library/Init/Data/Hashable.lean b/library/Init/Data/Hashable.lean
index 018003b146..1bcfeed4fc 100644
--- a/library/Init/Data/Hashable.lean
+++ b/library/Init/Data/Hashable.lean
@@ -14,10 +14,10 @@ class Hashable (α : Type u) :=
 export Hashable (hash)
 
 @[extern "lean_usize_mix_hash"]
-constant mixHash (u₁ u₂ : USize) : USize := default _
+constant mixHash (u₁ u₂ : USize) : USize := arbitrary _
 
 @[extern "lean_string_hash"]
-protected constant String.hash (s : String) : USize := default _
+protected constant String.hash (s : String) : USize := arbitrary _
 instance : Hashable String := ⟨String.hash⟩
 
 protected def Nat.hash (n : Nat) : USize :=
diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean
index ec12d6f74c..fc3b9c7668 100644
--- a/library/Init/Data/PersistentArray/Basic.lean
+++ b/library/Init/Data/PersistentArray/Basic.lean
@@ -147,7 +147,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
   if h : cs.size ≠ 0 then
     let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩;
     let last := cs.get idx;
-    let cs   := cs.set idx (default _);
+    let cs   := cs.set idx (arbitrary _);
     match popLeaf last with
     | (none,   _)       => (none, emptyArray)
     | (some l, newLast) =>
diff --git a/library/Init/Data/Random.lean b/library/Init/Data/Random.lean
index 2f9d9b2cbc..8d8bf33470 100644
--- a/library/Init/Data/Random.lean
+++ b/library/Init/Data/Random.lean
@@ -110,7 +110,7 @@ def IO.mkStdGenRef : IO (IO.Ref StdGen) :=
 IO.mkRef mkStdGen
 
 @[init IO.mkStdGenRef]
-constant IO.stdGenRef : IO.Ref StdGen := default _
+constant IO.stdGenRef : IO.Ref StdGen := arbitrary _
 
 def IO.setRandSeed (n : Nat) : IO Unit :=
 IO.stdGenRef.set (mkStdGen n)
diff --git a/library/Init/Data/String/Basic.lean b/library/Init/Data/String/Basic.lean
index 23fe4a213d..15b4c3e384 100644
--- a/library/Init/Data/String/Basic.lean
+++ b/library/Init/Data/String/Basic.lean
@@ -79,7 +79,7 @@ utf8ByteSize s
 {str := s, startPos := 0, stopPos := s.bsize}
 
 private def utf8GetAux : List Char → Pos → Pos → Char
-| [],    i, p => default Char
+| [],    i, p => arbitrary Char
 | c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p
 
 @[extern "lean_string_utf8_get"]
diff --git a/library/Init/Data/UInt.lean b/library/Init/Data/UInt.lean
index 4199d6d16e..1ab190960e 100644
--- a/library/Init/Data/UInt.lean
+++ b/library/Init/Data/UInt.lean
@@ -274,9 +274,9 @@ def USize.ofUInt32 (a : UInt32) : USize := USize.ofNat (UInt32.toNat a)
 def USize.ofUInt64 (a : UInt64) : USize := USize.ofNat (UInt64.toNat a)
 -- TODO(Leo): give reference implementation for shift_left and shift_right, and define them for other UInt types
 @[extern c inline "#1 << #2"]
-constant USize.shift_left (a b : USize) : USize := USize.ofNat (default _)
+constant USize.shift_left (a b : USize) : USize := USize.ofNat (arbitrary _)
 @[extern c inline "#1 >> #2"]
-constant USize.shift_right (a b : USize) : USize := USize.ofNat (default _)
+constant USize.shift_right (a b : USize) : USize := USize.ofNat (arbitrary _)
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
diff --git a/library/Init/Fix.lean b/library/Init/Fix.lean
index 7a9dda78f1..90f1a91a89 100644
--- a/library/Init/Fix.lean
+++ b/library/Init/Fix.lean
@@ -19,10 +19,10 @@ bfix1 base rec usizeSz
 fixCore1 base rec
 
 @[inline] def fix1 {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
-fixCore1 (fun _ => default β) rec
+fixCore1 (fun _ => arbitrary β) rec
 
 @[inline] def fix {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
-fixCore1 (fun _ => default β) rec
+fixCore1 (fun _ => arbitrary β) rec
 
 def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : Nat → α₁ → α₂ → β
 | 0,   a₁, a₂ => base a₁ a₂
@@ -33,7 +33,7 @@ def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (
 bfix2 base rec usizeSz
 
 @[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
-fixCore2 (fun _ _ => default β) rec
+fixCore2 (fun _ _ => arbitrary β) rec
 
 def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : Nat → α₁ → α₂ → α₃ → β
 | 0,   a₁, a₂, a₃ => base a₁ a₂ a₃
@@ -44,7 +44,7 @@ def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ 
 bfix3 base rec usizeSz
 
 @[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
-fixCore3 (fun _ _ _ => default β) rec
+fixCore3 (fun _ _ _ => arbitrary β) rec
 
 def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : Nat → α₁ → α₂ → α₃ → α₄ → β
 | 0,   a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄
@@ -55,7 +55,7 @@ def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → 
 bfix4 base rec usizeSz
 
 @[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
-fixCore4 (fun _ _ _ _ => default β) rec
+fixCore4 (fun _ _ _ _ => arbitrary β) rec
 
 def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
 | 0,   a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅
@@ -66,7 +66,7 @@ def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂
 bfix5 base rec usizeSz
 
 @[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
-fixCore5 (fun _ _ _ _ _ => default β) rec
+fixCore5 (fun _ _ _ _ _ => arbitrary β) rec
 
 def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
 | 0,   a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆
@@ -77,4 +77,4 @@ def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ →
 bfix6 base rec usizeSz
 
 @[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
-fixCore6 (fun _ _ _ _ _ _ => default β) rec
+fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec
diff --git a/library/Init/Lean/AbstractMetavarContext.lean b/library/Init/Lean/AbstractMetavarContext.lean
index a22fb1394b..0a98aaf084 100644
--- a/library/Init/Lean/AbstractMetavarContext.lean
+++ b/library/Init/Lean/AbstractMetavarContext.lean
@@ -85,7 +85,7 @@ structure MetavarDecl :=
 namespace MetavarDecl
 
 instance : Inhabited MetavarDecl :=
-⟨⟨default _, default _, default _, false⟩⟩
+⟨⟨arbitrary _, arbitrary _, arbitrary _, false⟩⟩
 
 end MetavarDecl
 
diff --git a/library/Init/Lean/Attributes.lean b/library/Init/Lean/Attributes.lean
index d69e4b8e3a..08f4ae362e 100644
--- a/library/Init/Lean/Attributes.lean
+++ b/library/Init/Lean/Attributes.lean
@@ -26,19 +26,19 @@ structure AttributeImpl :=
 (applicationTime := AttributeApplicationTime.afterTypeChecking)
 
 instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
-⟨{ name := default _, descr := default _, add := fun env _ _ _ => pure env }⟩
+⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩
 
 def mkAttributeMapRef : IO (IO.Ref (HashMap Name AttributeImpl)) :=
 IO.mkRef {}
 
 @[init mkAttributeMapRef]
-constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := default _
+constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := arbitrary _
 
 def mkAttributeArrayRef : IO (IO.Ref (Array AttributeImpl)) :=
 IO.mkRef #[]
 
 @[init mkAttributeArrayRef]
-constant attributeArrayRef : IO.Ref (Array AttributeImpl) := default _
+constant attributeArrayRef : IO.Ref (Array AttributeImpl) := arbitrary _
 
 /- Low level attribute registration function. -/
 def registerAttribute (attr : AttributeImpl) : IO Unit :=
@@ -174,7 +174,7 @@ do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension
 
 namespace TagAttribute
 
-instance : Inhabited TagAttribute := ⟨{attr := default _, ext := default _}⟩
+instance : Inhabited TagAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
 
 def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
 match env.getModuleIdxFor decl with
@@ -225,12 +225,12 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
 
 namespace ParametricAttribute
 
-instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := default _, ext := default _}⟩
+instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
 
 def getParam {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
 match env.getModuleIdxFor decl with
 | some modIdx =>
-  match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with
+  match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
   | some (_, val) => some val
   | none          => none
 | none        => (attr.ext.getState env).find decl
@@ -279,12 +279,12 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
 
 namespace EnumAttributes
 
-instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := default _}⟩
+instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := arbitrary _}⟩
 
 def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
 match env.getModuleIdxFor decl with
 | some modIdx =>
-  match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with
+  match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
   | some (_, val) => some val
   | none          => none
 | none        => (attr.ext.getState env).find decl
diff --git a/library/Init/Lean/AuxRecursor.lean b/library/Init/Lean/AuxRecursor.lean
index b4e9ba14cc..5a822fa3c0 100644
--- a/library/Init/Lean/AuxRecursor.lean
+++ b/library/Init/Lean/AuxRecursor.lean
@@ -12,7 +12,7 @@ def mkAuxRecursorExtension : IO TagDeclarationExtension :=
 mkTagDeclarationExtension `auxRec
 
 @[init mkAuxRecursorExtension]
-constant auxRecExt : TagDeclarationExtension := default _
+constant auxRecExt : TagDeclarationExtension := arbitrary _
 
 @[export lean_mark_aux_recursor]
 def markAuxRecursor (env : Environment) (n : Name) : Environment :=
@@ -26,7 +26,7 @@ def mkNoConfusionExtension : IO TagDeclarationExtension :=
 mkTagDeclarationExtension `noConf
 
 @[init mkNoConfusionExtension]
-constant noConfusionExt : TagDeclarationExtension := default _
+constant noConfusionExt : TagDeclarationExtension := arbitrary _
 
 @[export lean_mark_no_confusion]
 def markNoConfusion (env : Environment) (n : Name) : Environment :=
diff --git a/library/Init/Lean/Class.lean b/library/Init/Lean/Class.lean
index 9e911e33b6..9607e589e3 100644
--- a/library/Init/Lean/Class.lean
+++ b/library/Init/Lean/Class.lean
@@ -57,7 +57,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkClassExtension]
-constant classExtension : SimplePersistentEnvExtension ClassEntry ClassState := default _
+constant classExtension : SimplePersistentEnvExtension ClassEntry ClassState := arbitrary _
 
 @[export lean_is_class]
 def isClass (env : Environment) (n : Name) : Bool :=
diff --git a/library/Init/Lean/Compiler/ClosedTermCache.lean b/library/Init/Lean/Compiler/ClosedTermCache.lean
index 9afc4d4333..5922ade937 100644
--- a/library/Init/Lean/Compiler/ClosedTermCache.lean
+++ b/library/Init/Lean/Compiler/ClosedTermCache.lean
@@ -20,7 +20,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkClosedTermCacheExtension]
-constant closedTermCacheExt : SimplePersistentEnvExtension (Expr × Name) ClosedTermCache := default _
+constant closedTermCacheExt : SimplePersistentEnvExtension (Expr × Name) ClosedTermCache := arbitrary _
 
 @[export lean_cache_closed_term_name]
 def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=
diff --git a/library/Init/Lean/Compiler/ExportAttr.lean b/library/Init/Lean/Compiler/ExportAttr.lean
index b6f5e97e98..d3428cd375 100644
--- a/library/Init/Lean/Compiler/ExportAttr.lean
+++ b/library/Init/Lean/Compiler/ExportAttr.lean
@@ -26,7 +26,7 @@ registerParametricAttribute `export "name to be used by code generators" $ fun _
   | _ => Except.error "unexpected kind of argument"
 
 @[init mkExportAttr]
-constant exportAttr : ParametricAttribute Name := default _
+constant exportAttr : ParametricAttribute Name := arbitrary _
 
 @[export lean_get_export_name_for]
 def getExportNameFor (env : Environment) (n : Name) : Option Name :=
diff --git a/library/Init/Lean/Compiler/ExternAttr.lean b/library/Init/Lean/Compiler/ExternAttr.lean
index e1647cbe78..59671cc251 100644
--- a/library/Init/Lean/Compiler/ExternAttr.lean
+++ b/library/Init/Lean/Compiler/ExternAttr.lean
@@ -78,7 +78,7 @@ match s with
 | _ => Except.error "unexpected kind of argument"
 
 @[extern "lean_add_extern"]
-constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := default _
+constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := arbitrary _
 
 def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
 registerParametricAttribute `extern "builtin and foreign functions"
@@ -90,7 +90,7 @@ registerParametricAttribute `extern "builtin and foreign functions"
       pure env)
 
 @[init mkExternAttr]
-constant externAttr : ParametricAttribute ExternAttrData := default _
+constant externAttr : ParametricAttribute ExternAttrData := arbitrary _
 
 @[export lean_get_extern_attr_data]
 def getExternAttrData (env : Environment) (n : Name) : Option ExternAttrData :=
diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/library/Init/Lean/Compiler/IR/Basic.lean
index 2ddfc8f075..cb6ad1bb26 100644
--- a/library/Init/Lean/Compiler/IR/Basic.lean
+++ b/library/Init/Lean/Compiler/IR/Basic.lean
@@ -294,7 +294,7 @@ abbrev Alt := AltCore FnBody
 @[matchPattern] abbrev Alt.default := @AltCore.default FnBody
 
 instance altInh : Inhabited Alt :=
-⟨Alt.default (default _)⟩
+⟨Alt.default (arbitrary _)⟩
 
 def FnBody.isTerminal : FnBody → Bool
 | FnBody.case _ _ _ _  => true
@@ -376,7 +376,7 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
   if i == 0 then b
   else
     let i         := i - 1;
-    let (curr, a) := a.swapAt! i (default _);
+    let (curr, a) := a.swapAt! i (arbitrary _);
     let b         := curr.setBody b;
     reshapeAux a i b
 
@@ -402,7 +402,7 @@ inductive Decl
 namespace Decl
 
 instance : Inhabited Decl :=
-⟨fdecl (default _) (default _) IRType.irrelevant (default _)⟩
+⟨fdecl (arbitrary _) (arbitrary _) IRType.irrelevant (arbitrary _)⟩
 
 def name : Decl → FunId
 | Decl.fdecl f _ _ _  => f
diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean
index cf059703e1..18b81300e8 100644
--- a/library/Init/Lean/Compiler/IR/Borrow.lean
+++ b/library/Init/Lean/Compiler/IR/Borrow.lean
@@ -126,7 +126,7 @@ ApplyParamMap.visitDecls decls map
 
 structure BorrowInfCtx :=
 (env : Environment)
-(currFn : FunId := default _) -- Function being analyzed.
+(currFn : FunId := arbitrary _) -- Function being analyzed.
 (paramSet : IndexSet := {}) -- Set of all function parameters in scope. This is used to implement the heuristic at `ownArgsUsingParams`
 
 structure BorrowInfState :=
diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean
index 82ff79cdab..b6dfdf8e5f 100644
--- a/library/Init/Lean/Compiler/IR/Boxing.lean
+++ b/library/Init/Lean/Compiler/IR/Boxing.lean
@@ -62,16 +62,16 @@ do let ps := decl.params;
         if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
         else do
           x ← mkFresh;
-          pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
+          pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (arbitrary _)), xs.push (Arg.var x)))
      (#[], #[]);
    r ← mkFresh;
-   let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
+   let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (arbitrary _));
    body ←
      if !decl.resultType.isScalar then do {
        pure $ reshape newVDecls (FnBody.ret (Arg.var r))
      } else do {
        newR ← mkFresh;
-       let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
+       let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (arbitrary _));
        pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
      };
    pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
@@ -106,7 +106,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
 (t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
 
 structure BoxingContext :=
-(f : FunId := default _) (localCtx : LocalContext := {}) (resultType : IRType := IRType.irrelevant) (decls : Array Decl) (env : Environment)
+(f : FunId := arbitrary _) (localCtx : LocalContext := {}) (resultType : IRType := IRType.irrelevant) (decls : Array Decl) (env : Environment)
 
 structure BoxingState :=
 (nextIdx : Index)
@@ -149,7 +149,7 @@ def getDecl (fid : FunId) : M Decl :=
 do ctx ← read;
    match findEnvDecl' ctx.env fid ctx.decls with
    | some decl => pure decl
-   | none      => pure (default _) -- unreachable if well-formed
+   | none      => pure (arbitrary _) -- unreachable if well-formed
 
 @[inline] def withParams {α : Type} (xs : Array Param) (k : M α) : M α :=
 adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addParams xs, .. ctx }) k
diff --git a/library/Init/Lean/Compiler/IR/CompilerM.lean b/library/Init/Lean/Compiler/IR/CompilerM.lean
index 665e1b90ad..54f271cb86 100644
--- a/library/Init/Lean/Compiler/IR/CompilerM.lean
+++ b/library/Init/Lean/Compiler/IR/CompilerM.lean
@@ -89,7 +89,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkDeclMapExtension]
-constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := default _
+constant declMapExt : SimplePersistentEnvExtension Decl DeclMap := arbitrary _
 
 @[export lean_ir_find_env_decl]
 def findEnvDecl (env : Environment) (n : Name) : Option Decl :=
diff --git a/library/Init/Lean/Compiler/IR/CtorLayout.lean b/library/Init/Lean/Compiler/IR/CtorLayout.lean
index 6e1e14dace..892dc2fad8 100644
--- a/library/Init/Lean/Compiler/IR/CtorLayout.lean
+++ b/library/Init/Lean/Compiler/IR/CtorLayout.lean
@@ -36,7 +36,7 @@ structure CtorLayout :=
 (scalarSize : Nat)
 
 @[extern "lean_ir_get_ctor_layout"]
-constant getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout := default _
+constant getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout := arbitrary _
 
 end IR
 end Lean
diff --git a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
index b7bec961e8..db15655e4f 100644
--- a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -106,7 +106,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkFunctionSummariesExtension]
-constant functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries := default _
+constant functionSummariesExt : SimplePersistentEnvExtension (FunId × Value) FunctionSummaries := arbitrary _
 
 def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environment :=
 functionSummariesExt.addEntry env (fid, v)
diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean
index 244d244d26..19f04d26dd 100644
--- a/library/Init/Lean/Compiler/IR/EmitC.lean
+++ b/library/Init/Lean/Compiler/IR/EmitC.lean
@@ -26,7 +26,7 @@ structure Context :=
 (env        : Environment)
 (modName    : Name)
 (jpMap      : JPParamsMap := {})
-(mainFn     : FunId := default _)
+(mainFn     : FunId := arbitrary _)
 (mainParams : Array Param := #[])
 
 abbrev M := ReaderT Context (EStateM String String)
diff --git a/library/Init/Lean/Compiler/IR/RC.lean b/library/Init/Lean/Compiler/IR/RC.lean
index cb68a1ee25..8dee750e92 100644
--- a/library/Init/Lean/Compiler/IR/RC.lean
+++ b/library/Init/Lean/Compiler/IR/RC.lean
@@ -33,7 +33,7 @@ structure Context :=
 def getDecl (ctx : Context) (fid : FunId) : Decl :=
  match findEnvDecl' ctx.env fid ctx.decls with
 | some decl => decl
-| none      => default _ -- unreachable if well-formed
+| none      => arbitrary _ -- unreachable if well-formed
 
 def getVarInfo (ctx : Context) (x : VarId) : VarInfo :=
 match ctx.varMap.find x with
diff --git a/library/Init/Lean/Compiler/IR/UnboxResult.lean b/library/Init/Lean/Compiler/IR/UnboxResult.lean
index 44005d17b5..63054ebae2 100644
--- a/library/Init/Lean/Compiler/IR/UnboxResult.lean
+++ b/library/Init/Lean/Compiler/IR/UnboxResult.lean
@@ -23,7 +23,7 @@ registerTagAttribute `unbox "compiler tries to unbox result values if their type
     | _ => Except.error "constant must be an inductive type"
 
 @[init mkUnboxAttr]
-constant unboxAttr : TagAttribute := default _
+constant unboxAttr : TagAttribute := arbitrary _
 
 def hasUnboxAttr (env : Environment) (n : Name) : Bool :=
 unboxAttr.hasTag env n
diff --git a/library/Init/Lean/Compiler/ImplementedByAttr.lean b/library/Init/Lean/Compiler/ImplementedByAttr.lean
index 053fd673da..89d18292a7 100644
--- a/library/Init/Lean/Compiler/ImplementedByAttr.lean
+++ b/library/Init/Lean/Compiler/ImplementedByAttr.lean
@@ -24,7 +24,7 @@ registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) f
     | _ => Except.error "expected identifier"
 
 @[init mkImplementedByAttr]
-constant implementedByAttr : ParametricAttribute Name := default _
+constant implementedByAttr : ParametricAttribute Name := arbitrary _
 
 @[export lean_get_implemented_by]
 def getImplementedBy (env : Environment) (n : Name) : Option Name :=
diff --git a/library/Init/Lean/Compiler/InitAttr.lean b/library/Init/Lean/Compiler/InitAttr.lean
index 5412a4b5da..9ac72125e3 100644
--- a/library/Init/Lean/Compiler/InitAttr.lean
+++ b/library/Init/Lean/Compiler/InitAttr.lean
@@ -44,7 +44,7 @@ registerParametricAttribute `init "initialization procedure for global reference
       | _ => Except.error "unexpected kind of argument"
 
 @[init mkInitAttr]
-constant initAttr : ParametricAttribute Name := default _
+constant initAttr : ParametricAttribute Name := arbitrary _
 
 def isIOUnitInitFn (env : Environment) (fn : Name) : Bool :=
 match initAttr.getParam env fn with
diff --git a/library/Init/Lean/Compiler/InlineAttrs.lean b/library/Init/Lean/Compiler/InlineAttrs.lean
index 2699f063a3..dff9d02b41 100644
--- a/library/Init/Lean/Compiler/InlineAttrs.lean
+++ b/library/Init/Lean/Compiler/InlineAttrs.lean
@@ -37,7 +37,7 @@ registerEnumAttributes `inlineAttrs
   (fun env declName _ => checkIsDefinition env declName)
 
 @[init mkInlineAttrs]
-constant inlineAttrs : EnumAttributes InlineAttributeKind := default _
+constant inlineAttrs : EnumAttributes InlineAttributeKind := arbitrary _
 
 private partial def hasInlineAttrAux (env : Environment) (kind : InlineAttributeKind) : Name → Bool
 | n =>
diff --git a/library/Init/Lean/Compiler/NeverExtractAttr.lean b/library/Init/Lean/Compiler/NeverExtractAttr.lean
index c61f92dc0b..2aabdd9f4f 100644
--- a/library/Init/Lean/Compiler/NeverExtractAttr.lean
+++ b/library/Init/Lean/Compiler/NeverExtractAttr.lean
@@ -13,7 +13,7 @@ def mkNeverExtractAttr : IO TagAttribute :=
 registerTagAttribute `neverExtract "instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects."
 
 @[init mkNeverExtractAttr]
-constant neverExtractAttr : TagAttribute := default _
+constant neverExtractAttr : TagAttribute := arbitrary _
 
 private partial def hasNeverExtractAttributeAux (env : Environment) : Name → Bool
 | n =>
diff --git a/library/Init/Lean/Compiler/Specialize.lean b/library/Init/Lean/Compiler/Specialize.lean
index 4140366288..1593e82ab8 100644
--- a/library/Init/Lean/Compiler/Specialize.lean
+++ b/library/Init/Lean/Compiler/Specialize.lean
@@ -33,7 +33,7 @@ registerEnumAttributes `specializeAttrs
   (fun env declName _ => checkIsDefinition env declName)
 
 @[init mkSpecializeAttrs]
-constant specializeAttrs : EnumAttributes SpecializeAttributeKind := default _
+constant specializeAttrs : EnumAttributes SpecializeAttributeKind := arbitrary _
 
 private partial def hasSpecializeAttrAux (env : Environment) (kind : SpecializeAttributeKind) : Name → Bool
 | n => match specializeAttrs.getValue env n with
@@ -88,7 +88,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkSpecExtension]
-constant specExtension : SimplePersistentEnvExtension SpecEntry SpecState := default _
+constant specExtension : SimplePersistentEnvExtension SpecEntry SpecState := arbitrary _
 
 @[export lean_add_specialization_info]
 def addSpecializationInfo (env : Environment) (fn : Name) (info : SpecInfo) : Environment :=
diff --git a/library/Init/Lean/Declaration.lean b/library/Init/Lean/Declaration.lean
index 7a1f521216..3ec3cbccbc 100644
--- a/library/Init/Lean/Declaration.lean
+++ b/library/Init/Lean/Declaration.lean
@@ -181,10 +181,10 @@ def hints : ConstantInfo → ReducibilityHints
 | _                         => ReducibilityHints.opaque
 
 @[extern "lean_instantiate_type_lparams"]
-constant instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr := default _
+constant instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr := arbitrary _
 
 @[extern "lean_instantiate_value_lparams"]
-constant instantiateValueLevelParams (c : ConstantInfo) (ls : List Level) : Expr := default _
+constant instantiateValueLevelParams (c : ConstantInfo) (ls : List Level) : Expr := arbitrary _
 
 end ConstantInfo
 end Lean
diff --git a/library/Init/Lean/Elaborator/Alias.lean b/library/Init/Lean/Elaborator/Alias.lean
index a6602ce3b4..5da1a86973 100644
--- a/library/Init/Lean/Elaborator/Alias.lean
+++ b/library/Init/Lean/Elaborator/Alias.lean
@@ -26,7 +26,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkAliasExtension]
-constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := default _
+constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := arbitrary _
 
 /- Add alias `a` for `e` -/
 def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean
index 79f88b9ac2..e881023486 100644
--- a/library/Init/Lean/Elaborator/Basic.lean
+++ b/library/Init/Lean/Elaborator/Basic.lean
@@ -43,7 +43,7 @@ structure ElabScope :=
 
 namespace ElabScope
 
-instance : Inhabited ElabScope := ⟨{ cmd := "", header := default _ }⟩
+instance : Inhabited ElabScope := ⟨{ cmd := "", header := arbitrary _ }⟩
 
 end ElabScope
 
@@ -83,9 +83,9 @@ abbrev CommandElabTable : Type := SMap SyntaxNodeKind CommandElab
 def mkBuiltinTermElabTable : IO (IO.Ref TermElabTable) :=  IO.mkRef {}
 def mkBuiltinCommandElabTable : IO (IO.Ref CommandElabTable) := IO.mkRef {}
 @[init mkBuiltinTermElabTable]
-constant builtinTermElabTable : IO.Ref TermElabTable := default _
+constant builtinTermElabTable : IO.Ref TermElabTable := arbitrary _
 @[init mkBuiltinCommandElabTable]
-constant builtinCommandElabTable : IO.Ref CommandElabTable := default _
+constant builtinCommandElabTable : IO.Ref CommandElabTable := arbitrary _
 
 def addBuiltinTermElab (k : SyntaxNodeKind) (declName : Name) (elab : TermElab) : IO Unit :=
 do m ← builtinTermElabTable.get;
@@ -181,7 +181,7 @@ structure ElabAttribute (σ : Type) :=
 
 namespace ElabAttribute
 
-instance {σ} [Inhabited σ] : Inhabited (ElabAttribute σ) := ⟨{ attr := default _, ext := default _, kind := "" }⟩
+instance {σ} [Inhabited σ] : Inhabited (ElabAttribute σ) := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
 
 end ElabAttribute
 
@@ -213,13 +213,13 @@ abbrev TermElabAttribute := ElabAttribute TermElabTable
 def mkTermElabAttribute : IO TermElabAttribute :=
 mkElabAttribute `elabTerm "term" builtinTermElabTable
 @[init mkTermElabAttribute]
-constant termElabAttribute : TermElabAttribute := default _
+constant termElabAttribute : TermElabAttribute := arbitrary _
 
 abbrev CommandElabAttribute := ElabAttribute CommandElabTable
 def mkCommandElabAttribute : IO CommandElabAttribute :=
 mkElabAttribute `commandTerm "command" builtinCommandElabTable
 @[init mkCommandElabAttribute]
-constant commandElabAttribute : CommandElabAttribute := default _
+constant commandElabAttribute : CommandElabAttribute := arbitrary _
 
 namespace Elab
 def logMessage (msg : Message) : Elab Unit :=
@@ -398,7 +398,7 @@ do env ← mkEmptyEnvironment;
        | EStateM.Result.error _ s => pure (s.elabState.env, s.elabState.messages)
 
 instance {α} : Inhabited (Elab α) :=
-⟨fun _ => default _⟩
+⟨fun _ => arbitrary _⟩
 
 def mkFreshName : Elab Name :=
 modifyGet $ fun s => (s.ngen.curr, { ngen := s.ngen.next, .. s })
@@ -431,7 +431,7 @@ modifyGet $ fun s =>
   | { scopes := h::t, .. } =>
     let (a, h) := f h;
     (a, { scopes := h :: t, .. s })
-  | _ => (default _, s)
+  | _ => (arbitrary _, s)
 
 def localContext : Elab LocalContext :=
 do scope ← getScope; pure scope.lctx
@@ -515,7 +515,7 @@ match unsafeIO x with
 | Except.error e => throw (ElabException.io e)
 
 @[implementedBy runIOUnsafe]
-constant runIO {α : Type} (x : IO α) : Elab α := default _
+constant runIO {α : Type} (x : IO α) : Elab α := arbitrary _
 
 end Elab
 
diff --git a/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean b/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean
index 35de1a41d3..12709cf1d9 100644
--- a/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean
+++ b/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean
@@ -25,7 +25,7 @@ registerEnumAttributes `elaboratorStrategy
    (`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
 
 @[init mkElaboratorStrategyAttrs]
-constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := default _
+constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := arbitrary _
 
 @[export lean_get_elaborator_strategy]
 def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/library/Init/Lean/Elaborator/PreTerm.lean
index 18a6119743..1677a20d2a 100644
--- a/library/Init/Lean/Elaborator/PreTerm.lean
+++ b/library/Init/Lean/Elaborator/PreTerm.lean
@@ -11,7 +11,7 @@ namespace Lean
 abbrev PreTerm := Expr
 
 @[extern "lean_old_elaborate"]
-constant oldElaborateAux : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := default _
+constant oldElaborateAux : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := arbitrary _
 
 abbrev PreTermElab := SyntaxNode Expr → Elab PreTerm
 
@@ -20,7 +20,7 @@ abbrev PreTermElabTable : Type := HashMap SyntaxNodeKind PreTermElab
 def mkBuiltinPreTermElabTable : IO (IO.Ref PreTermElabTable) :=  IO.mkRef {}
 
 @[init mkBuiltinPreTermElabTable]
-constant builtinPreTermElabTable : IO.Ref PreTermElabTable := default _
+constant builtinPreTermElabTable : IO.Ref PreTermElabTable := arbitrary _
 
 def addBuiltinPreTermElab (k : SyntaxNodeKind) (declName : Name) (elab : PreTermElab) : IO Unit :=
 do m ← builtinPreTermElabTable.get;
diff --git a/library/Init/Lean/Environment.lean b/library/Init/Lean/Environment.lean
index e19424c30d..f3c494afbe 100644
--- a/library/Init/Lean/Environment.lean
+++ b/library/Init/Lean/Environment.lean
@@ -30,7 +30,7 @@ abbrev ConstMap := SMap Name ConstantInfo
 structure EnvironmentHeader :=
 (trustLevel   : UInt32     := 0)
 (quotInit     : Bool       := false)
-(mainModule   : Name       := default _)
+(mainModule   : Name       := arbitrary _)
 (imports      : Array Name := #[])
 
 /- TODO: mark opaque. -/
@@ -107,11 +107,11 @@ namespace Environment
 
 /- Type check given declaration and add it to the environment -/
 @[extern "lean_add_decl"]
-constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment := default _
+constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment := arbitrary _
 
 /- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
 @[extern "lean_compile_decl"]
-constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := default _
+constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := arbitrary _
 
 def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment :=
 do env ← addDecl env decl;
@@ -131,7 +131,7 @@ unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment
 { extensions := env.extensions.set! ext.idx (unsafeCast s), .. env }
 
 @[implementedBy setStateUnsafe]
-constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := default _
+constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := arbitrary _
 
 unsafe def getStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :=
 let s : EnvExtensionState := env.extensions.get! ext.idx;
@@ -148,7 +148,7 @@ constant getState {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :
   .. env }
 
 @[implementedBy modifyStateUnsafe]
-constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := default _
+constant modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment := arbitrary _
 
 end EnvExtension
 
@@ -156,10 +156,10 @@ private def mkEnvExtensionsRef : IO (IO.Ref (Array (EnvExtension EnvExtensionSta
 IO.mkRef #[]
 
 @[init mkEnvExtensionsRef]
-private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := default _
+private constant envExtensionsRef : IO.Ref (Array (EnvExtension EnvExtensionState)) := arbitrary _
 
 instance EnvExtension.Inhabited (σ : Type) [Inhabited σ] : Inhabited (EnvExtension σ) :=
-⟨{ idx := 0, stateInh := default _, mkInitial := default _ }⟩
+⟨{ idx := 0, stateInh := arbitrary _, mkInitial := arbitrary _ }⟩
 
 unsafe def registerEnvExtensionUnsafe {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) :=
 do initializing ← IO.initializing;
@@ -169,7 +169,7 @@ do initializing ← IO.initializing;
    let ext : EnvExtension σ := {
       idx        := idx,
       mkInitial  := mkInitial,
-      stateInh   := default _
+      stateInh   := arbitrary _
    };
    envExtensionsRef.modify (fun exts => exts.push (unsafeCast ext));
    pure ext
@@ -179,7 +179,7 @@ do initializing ← IO.initializing;
    1- Our implementation assumes the number of extensions does not change after an environment object is created.
    2- We do not use any synchronization primitive to access `envExtensionsRef`. -/
 @[implementedBy registerEnvExtensionUnsafe]
-constant registerEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) := default _
+constant registerEnvExtension {σ : Type} [Inhabited σ] (mkInitial : IO σ) : IO (EnvExtension σ) := arbitrary _
 
 private def mkInitialExtensionStates : IO (Array EnvExtensionState) :=
 do exts ← envExtensionsRef.get; exts.mapM $ fun ext => ext.mkInitial
@@ -217,12 +217,12 @@ def EnvExtensionEntry := NonScalar
 instance EnvExtensionEntry.inhabited : Inhabited EnvExtensionEntry := inferInstanceAs (Inhabited NonScalar)
 
 instance PersistentEnvExtensionState.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
-⟨{importedEntries := #[], state := default _ }⟩
+⟨{importedEntries := #[], state := arbitrary _ }⟩
 
 instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α σ) :=
-⟨{ toEnvExtension := { idx := 0, stateInh := default _, mkInitial := default _ },
-   name := default _,
-   addImportedFn := fun _ => default _,
+⟨{ toEnvExtension := { idx := 0, stateInh := arbitrary _, mkInitial := arbitrary _ },
+   name := arbitrary _,
+   addImportedFn := fun _ => arbitrary _,
    addEntryFn := fun s _ => s,
    exportEntriesFn := fun _ => #[],
    statsFn := fun _ => Format.nil }⟩
@@ -252,7 +252,7 @@ private def mkPersistentEnvExtensionsRef : IO (IO.Ref (Array (PersistentEnvExten
 IO.mkRef #[]
 
 @[init mkPersistentEnvExtensionsRef]
-private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := default _
+private constant persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionState)) := arbitrary _
 
 structure PersistentEnvExtensionDescr (α σ : Type) :=
 (name            : Name)
@@ -283,7 +283,7 @@ do pExts ← persistentEnvExtensionsRef.get;
    pure pExt
 
 @[implementedBy registerPersistentEnvExtensionUnsafe]
-constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := default _
+constant registerPersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α σ) : IO (PersistentEnvExtension α σ) := arbitrary _
 
 /- Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries. -/
 
@@ -395,7 +395,7 @@ def regModListExtension : IO (EnvExtension (List Modification)) :=
 registerEnvExtension (pure [])
 
 @[init regModListExtension]
-constant modListExtension : EnvExtension (List Modification) := default _
+constant modListExtension : EnvExtension (List Modification) := arbitrary _
 
 /- The C++ code uses this function to store the given modification object into the environment. -/
 @[export lean_environment_add_modification]
@@ -405,10 +405,10 @@ modListExtension.modifyState env $ fun mods => mod :: mods
 /- mkModuleData invokes this function to convert a list of modification objects into
    a serialized byte array. -/
 @[extern 2 "lean_serialize_modifications"]
-constant serializeModifications : List Modification → IO ByteArray := default _
+constant serializeModifications : List Modification → IO ByteArray := arbitrary _
 
 @[extern 3 "lean_perform_serialized_modifications"]
-constant performModifications : Environment → ByteArray → IO Environment := default _
+constant performModifications : Environment → ByteArray → IO Environment := arbitrary _
 
 /- Content of a .olean file.
    We use `compact.cpp` to generate the image of this object in disk. -/
@@ -419,12 +419,12 @@ structure ModuleData :=
 (serialized : ByteArray) -- Legacy support: serialized modification objects
 
 instance ModuleData.inhabited : Inhabited ModuleData :=
-⟨{imports := default _, constants := default _, entries := default _, serialized := default _}⟩
+⟨{imports := arbitrary _, constants := arbitrary _, entries := arbitrary _, serialized := arbitrary _}⟩
 
 @[extern 3 "lean_save_module_data"]
-constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := default _
+constant saveModuleData (fname : @& String) (m : ModuleData) : IO Unit := arbitrary _
 @[extern 2 "lean_read_module_data"]
-constant readModuleData (fname : @& String) : IO ModuleData := default _
+constant readModuleData (fname : @& String) : IO ModuleData := arbitrary _
 
 def mkModuleData (env : Environment) : IO ModuleData :=
 do pExts ← persistentEnvExtensionsRef.get;
@@ -520,7 +520,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init regNamespacesExtension]
-constant namespacesExt : SimplePersistentEnvExtension Name NameSet := default _
+constant namespacesExt : SimplePersistentEnvExtension Name NameSet := arbitrary _
 
 def registerNamespace (env : Environment) (n : Name) : Environment :=
 if (namespacesExt.getState env).contains n then env else namespacesExt.addEntry env n
diff --git a/library/Init/Lean/EqnCompiler/MatchPattern.lean b/library/Init/Lean/EqnCompiler/MatchPattern.lean
index d1ce445bf6..c89ffd702d 100644
--- a/library/Init/Lean/EqnCompiler/MatchPattern.lean
+++ b/library/Init/Lean/EqnCompiler/MatchPattern.lean
@@ -13,7 +13,7 @@ def mkMatchPatternAttr : IO TagAttribute :=
 registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
 
 @[init mkMatchPatternAttr]
-constant matchPatternAttr : TagAttribute := default _
+constant matchPatternAttr : TagAttribute := arbitrary _
 
 @[export lean_has_match_pattern_attribute]
 def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=
diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean
index 5038865679..1b528f785b 100644
--- a/library/Init/Lean/Expr.lean
+++ b/library/Init/Lean/Expr.lean
@@ -82,7 +82,7 @@ attribute [extern "lean_expr_mk_proj"]   Expr.proj
 
 -- deprecated Constructor
 @[extern "lean_expr_local"]
-constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := default _
+constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := arbitrary _
 
 def mkApp (f : Expr) (args : Array Expr) : Expr :=
 args.foldl Expr.app f
@@ -102,43 +102,43 @@ revArgs.foldr (fun a r => Expr.app r a) fn
 
 namespace Expr
 @[extern "lean_expr_hash"]
-constant hash (n : @& Expr) : USize := default USize
+constant hash (n : @& Expr) : USize := arbitrary USize
 
 instance : Hashable Expr := ⟨Expr.hash⟩
 
 -- TODO: implement it in Lean
 @[extern "lean_expr_dbg_to_string"]
-constant dbgToString (e : @& Expr) : String := default String
+constant dbgToString (e : @& Expr) : String := arbitrary String
 
 @[extern "lean_expr_quick_lt"]
-constant quickLt (a : @& Expr) (b : @& Expr) : Bool := default _
+constant quickLt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
 
 @[extern "lean_expr_lt"]
-constant lt (a : @& Expr) (b : @& Expr) : Bool := default _
+constant lt (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
 
 /- Return true iff `a` and `b` are alpha equivalent.
    Binder annotations are ignored. -/
 @[extern "lean_expr_eqv"]
-constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
+constant eqv (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
 
 instance : HasBeq Expr := ⟨Expr.eqv⟩
 
 /- Return true iff `a` and `b` are equal.
    Binder names and annotations are taking into account. -/
 @[extern "lean_expr_equal"]
-constant equal (a : @& Expr) (b : @& Expr) : Bool := default _
+constant equal (a : @& Expr) (b : @& Expr) : Bool := arbitrary _
 
 @[extern "lean_expr_has_expr_mvar"]
-constant hasExprMVar (a : @& Expr) : Bool := default _
+constant hasExprMVar (a : @& Expr) : Bool := arbitrary _
 
 @[extern "lean_expr_has_level_mvar"]
-constant hasLevelMVar (a : @& Expr) : Bool := default _
+constant hasLevelMVar (a : @& Expr) : Bool := arbitrary _
 
 @[inline] def hasMVar (a : Expr) : Bool :=
 a.hasExprMVar || a.hasLevelMVar
 
 @[extern "lean_expr_has_fvar"]
-constant hasFVar (a : @& Expr) : Bool := default _
+constant hasFVar (a : @& Expr) : Bool := arbitrary _
 
 def isSort : Expr → Bool
 | sort _ => true
@@ -308,30 +308,30 @@ def letName! : Expr → Name
 /-- Instantiate the loose bound variables in `e` using `subst`.
     That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]
-constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := default _
+constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _
 
 @[extern "lean_expr_instantiate1"]
-constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := default _
+constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := arbitrary _
 
 /-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/
 @[extern "lean_expr_instantiate_rev"]
-constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := default _
+constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := arbitrary _
 
 /-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`.
     Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/
 @[extern "lean_expr_instantiate_range"]
-constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : Array Expr) : Expr := default _
+constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : Array Expr) : Expr := arbitrary _
 
 /-- Replace free variables `xs` with loose bound variables. -/
 @[extern "lean_expr_abstract"]
-constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := default _
+constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := arbitrary _
 
 /-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
 @[extern "lean_expr_abstract_range"]
-constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := default _
+constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := arbitrary _
 
 @[extern "lean_instantiate_lparams"]
-constant instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr := default _
+constant instantiateLevelParams (e : Expr) (paramNames : List Name) (lvls : List Level) : Expr := arbitrary _
 
 instance : HasToString Expr :=
 ⟨Expr.dbgToString⟩
@@ -377,7 +377,7 @@ protected def beq : ExprStructEq → ExprStructEq → Bool
 protected def hash : ExprStructEq → USize
 | ⟨e⟩ => e.hash
 
-instance : Inhabited ExprStructEq := ⟨{ val := default _ }⟩
+instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩
 instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩
 instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
 instance : HasToString ExprStructEq := ⟨fun e => toString e.val⟩
diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean
index f63fb1be22..efb8a719a2 100644
--- a/library/Init/Lean/Level.lean
+++ b/library/Init/Lean/Level.lean
@@ -144,12 +144,12 @@ def instantiate (s : Name → Option Level) : Level → Level
 | l           => l
 
 @[extern "lean_level_hash"]
-protected constant hash (n : @& Level) : USize := default USize
+protected constant hash (n : @& Level) : USize := arbitrary USize
 
 instance hashable : Hashable Level := ⟨Level.hash⟩
 
 @[extern "lean_level_eq"]
-protected constant beq (a : @& Level) (b : @& Level) : Bool := default _
+protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _
 
 instance : HasBeq Level := ⟨Level.beq⟩
 
diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean
index 4737374c66..8cc88b0307 100644
--- a/library/Init/Lean/LocalContext.lean
+++ b/library/Init/Lean/LocalContext.lean
@@ -15,7 +15,7 @@ inductive LocalDecl
 | ldecl (index : Nat) (name : Name) (userName : Name) (type : Expr) (value : Expr)
 
 namespace LocalDecl
-instance : Inhabited LocalDecl := ⟨ldecl (default _) (default _) (default _) (default _) (default _)⟩
+instance : Inhabited LocalDecl := ⟨ldecl (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _) (arbitrary _)⟩
 
 def isLet : LocalDecl → Bool
 | cdecl _ _ _ _ _ => false
diff --git a/library/Init/Lean/Message.lean b/library/Init/Lean/Message.lean
index e0722220aa..231ef114fa 100644
--- a/library/Init/Lean/Message.lean
+++ b/library/Init/Lean/Message.lean
@@ -40,7 +40,7 @@ inductive MessageData
 
 namespace MessageData
 
-instance : Inhabited MessageData := ⟨MessageData.ofFormat (default _)⟩
+instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
 
 partial def formatAux : Option (Environment × MetavarContext × LocalContext) → MessageData → Format
 | _, ofFormat fmt                  => fmt
@@ -84,7 +84,7 @@ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
   (if msg.caption == "" then "" else msg.caption ++ ":\n") ++ toString (fmt msg.data))
 
 instance : Inhabited Message :=
-⟨{ fileName := "", pos := ⟨0, 1⟩, data := default _}⟩
+⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
 
 instance : HasToString Message :=
 ⟨Message.toString⟩
diff --git a/library/Init/Lean/Modifiers.lean b/library/Init/Lean/Modifiers.lean
index 91f64829be..8738efcbc8 100644
--- a/library/Init/Lean/Modifiers.lean
+++ b/library/Init/Lean/Modifiers.lean
@@ -12,7 +12,7 @@ def mkProtectedExtension : IO TagDeclarationExtension :=
 mkTagDeclarationExtension `protected
 
 @[init mkProtectedExtension]
-constant protectedExt : TagDeclarationExtension := default _
+constant protectedExt : TagDeclarationExtension := arbitrary _
 
 @[export lean_add_protected]
 def addProtected (env : Environment) (n : Name) : Environment :=
@@ -26,7 +26,7 @@ def mkPrivateExtension : IO (EnvExtension Nat) :=
 registerEnvExtension (pure 1)
 
 @[init mkPrivateExtension]
-constant privateExt : EnvExtension Nat := default _
+constant privateExt : EnvExtension Nat := arbitrary _
 
 /- Private name support.
 
diff --git a/library/Init/Lean/Name.lean b/library/Init/Lean/Name.lean
index 1bfd0c7216..b527084425 100644
--- a/library/Init/Lean/Name.lean
+++ b/library/Init/Lean/Name.lean
@@ -38,7 +38,7 @@ instance stringToName : HasCoe String Name :=
 
 namespace Name
 @[extern "lean_name_hash_usize"]
-constant hash (n : @& Name) : USize := default _
+constant hash (n : @& Name) : USize := arbitrary _
 
 instance : Hashable Name :=
 ⟨Name.hash⟩
diff --git a/library/Init/Lean/Options.lean b/library/Init/Lean/Options.lean
index 8004b3a2ae..04cd006308 100644
--- a/library/Init/Lean/Options.lean
+++ b/library/Init/Lean/Options.lean
@@ -28,7 +28,7 @@ private def initOptionDeclsRef : IO (IO.Ref OptionDecls) :=
 IO.mkRef (mkNameMap OptionDecl)
 
 @[init initOptionDeclsRef]
-private constant optionDeclsRef : IO.Ref OptionDecls := default _
+private constant optionDeclsRef : IO.Ref OptionDecls := arbitrary _
 
 def registerOption (name : Name) (decl : OptionDecl) : IO Unit :=
 do decls ← optionDeclsRef.get;
diff --git a/library/Init/Lean/Parser/Command.lean b/library/Init/Lean/Parser/Command.lean
index 2a9ffd12df..3906d4521d 100644
--- a/library/Init/Lean/Parser/Command.lean
+++ b/library/Init/Lean/Parser/Command.lean
@@ -10,7 +10,7 @@ namespace Lean
 namespace Parser
 
 @[init mkBuiltinParsingTablesRef]
-constant builtinCommandParsingTable : IO.Ref ParsingTables := default _
+constant builtinCommandParsingTable : IO.Ref ParsingTables := arbitrary _
 
 @[init] def regBuiltinCommandParserAttr : IO Unit :=
 registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommandParsingTable
@@ -19,7 +19,7 @@ def mkCommandParserAttribute : IO ParserAttribute :=
 registerParserAttribute `commandParser "command" "command parser" (some builtinCommandParsingTable)
 
 @[init mkCommandParserAttribute]
-constant commandParserAttribute : ParserAttribute := default _
+constant commandParserAttribute : ParserAttribute := arbitrary _
 
 @[inline] def commandParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 { fn := fun _ => commandParserAttribute.runParser rbp }
diff --git a/library/Init/Lean/Parser/Level.lean b/library/Init/Lean/Parser/Level.lean
index a573172f45..be51d670d7 100644
--- a/library/Init/Lean/Parser/Level.lean
+++ b/library/Init/Lean/Parser/Level.lean
@@ -10,7 +10,7 @@ namespace Lean
 namespace Parser
 
 @[init mkBuiltinParsingTablesRef]
-constant builtinLevelParsingTable : IO.Ref ParsingTables := default _
+constant builtinLevelParsingTable : IO.Ref ParsingTables := arbitrary _
 
 @[init] def regBuiltinLevelParserAttr : IO Unit :=
 registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
@@ -19,7 +19,7 @@ def mkLevelParserAttribute : IO ParserAttribute :=
 registerParserAttribute `levelParser "level" "universe level parser" (some builtinLevelParsingTable)
 
 @[init mkLevelParserAttribute]
-constant levelParserAttribute : ParserAttribute := default _
+constant levelParserAttribute : ParserAttribute := arbitrary _
 
 @[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 { fn := fun _ => levelParserAttribute.runParser rbp }
diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean
index 0fcaac1caf..a0d896cb1a 100644
--- a/library/Init/Lean/Parser/Parser.lean
+++ b/library/Init/Lean/Parser/Parser.lean
@@ -77,7 +77,7 @@ structure ParserContextCore :=
 (tokens   : TokenTable)
 
 instance ParserContextCore.inhabited : Inhabited ParserContextCore :=
-⟨{ input := "", fileName := "", fileMap := default _, tokens := {} }⟩
+⟨{ input := "", fileName := "", fileMap := arbitrary _, tokens := {} }⟩
 
 structure ParserContext extends ParserContextCore :=
 (env      : Environment)
@@ -1327,7 +1327,7 @@ def mkBuiltinTokenTable : IO (IO.Ref TokenTable) :=
 IO.mkRef {}
 
 @[init mkBuiltinTokenTable]
-constant builtinTokenTable : IO.Ref TokenTable := default _
+constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
 
 def mkImportedTokenTable (es : Array (Array TokenConfig)) : IO TokenTable :=
 do table ← builtinTokenTable.get;
@@ -1341,7 +1341,7 @@ structure TokenTableAttribute :=
 (attr : AttributeImpl)
 (ext  : PersistentEnvExtension TokenConfig TokenTable)
 
-instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ attr := default _, ext := default _ }⟩
+instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _ }⟩
 
 section
 set_option compiler.extract_closed false
@@ -1362,12 +1362,12 @@ do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnv
 end
 
 @[init mkTokenTableAttribute]
-constant tokenTableAttribute : TokenTableAttribute := default _
+constant tokenTableAttribute : TokenTableAttribute := arbitrary _
 
 /- Global table with all SyntaxNodeKind's -/
 def mkSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
 @[init mkSyntaxNodeKindSetRef]
-constant syntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := default _
+constant syntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
 
 def updateSyntaxNodeKinds (pinfo : ParserInfo) : IO Unit :=
 syntaxNodeKindSetRef.modify pinfo.updateKindSet
@@ -1487,7 +1487,7 @@ match unsafeIO (do tables ← ref.get; pure $ prattParser kind tables a c s) wit
 | _           => s.mkError "failed to access builtin reference"
 
 @[implementedBy runBuiltinParserUnsafe]
-constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := default _
+constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := arbitrary _
 
 inductive ParserAttributeEntry
 | leading (n : Name)
@@ -1498,7 +1498,7 @@ structure ParserAttribute :=
 (ext  : PersistentEnvExtension ParserAttributeEntry ParsingTables)
 (kind : String)
 
-instance ParserAttribute.inhabited : Inhabited ParserAttribute := ⟨{ attr := default _, ext := default _, kind := "" }⟩
+instance ParserAttribute.inhabited : Inhabited ParserAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
 
 /-
 This is just the basic skeleton where we create an
diff --git a/library/Init/Lean/Parser/Term.lean b/library/Init/Lean/Parser/Term.lean
index 140305d566..2e47f465b5 100644
--- a/library/Init/Lean/Parser/Term.lean
+++ b/library/Init/Lean/Parser/Term.lean
@@ -11,7 +11,7 @@ namespace Lean
 namespace Parser
 
 @[init mkBuiltinParsingTablesRef]
-constant builtinTermParsingTable : IO.Ref ParsingTables := default _
+constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _
 
 @[init] def regBuiltinTermParserAttr : IO Unit :=
 registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
@@ -20,7 +20,7 @@ def mkTermParserAttribute : IO ParserAttribute :=
 registerParserAttribute `termParser "term" "term parser" (some builtinTermParsingTable)
 
 @[init mkTermParserAttribute]
-constant termParserAttribute : ParserAttribute := default _
+constant termParserAttribute : ParserAttribute := arbitrary _
 
 @[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 { fn := fun _ => termParserAttribute.runParser rbp }
diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean
index b872c601cd..33a1f1b82d 100644
--- a/library/Init/Lean/Path.lean
+++ b/library/Init/Lean/Path.lean
@@ -23,7 +23,7 @@ do curr ← realPathNormalized ".";
    IO.mkRef #[curr]
 
 @[init mkSearchPathRef]
-constant searchPathRef : IO.Ref (Array String) := default _
+constant searchPathRef : IO.Ref (Array String) := arbitrary _
 
 def setSearchPath (s : List String) : IO Unit :=
 do s ← s.mapM realPathNormalized;
diff --git a/library/Init/Lean/ProjFns.lean b/library/Init/Lean/ProjFns.lean
index 91d28bd79a..c1457d16be 100644
--- a/library/Init/Lean/ProjFns.lean
+++ b/library/Init/Lean/ProjFns.lean
@@ -17,7 +17,7 @@ structure ProjectionFunctionInfo :=
 (fromClass : Bool) -- `true` if the structure is a class
 
 instance ProjectionFunctionInfo.inhabited : Inhabited ProjectionFunctionInfo :=
-⟨{ ctorName := default _, nparams := default _, i := 0, fromClass := false }⟩
+⟨{ ctorName := arbitrary _, nparams := arbitrary _, i := 0, fromClass := false }⟩
 
 def mkProjectionFnInfoExtension : IO (SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo)) :=
 registerSimplePersistentEnvExtension {
@@ -28,7 +28,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init mkProjectionFnInfoExtension]
-constant projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) := default _
+constant projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) := arbitrary _
 
 @[export lean_add_projection_info]
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
@@ -40,14 +40,14 @@ namespace Environment
 def getProjectionFnInfo (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
 match env.getModuleIdxFor projName with
 | some modIdx =>
-  match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, default _) (fun a b => Name.quickLt a.1 b.1) with
+  match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
   | some e => some e.2
   | none   => none
 | none        => (projectionFnInfoExt.getState env).find projName
 
 def isProjectionFn (env : Environment) (n : Name) : Bool :=
 match env.getModuleIdxFor n with
-| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, default _) (fun a b => Name.quickLt a.1 b.1)
+| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, arbitrary _) (fun a b => Name.quickLt a.1 b.1)
 | none        => (projectionFnInfoExt.getState env).contains n
 
 end Environment
diff --git a/library/Init/Lean/ReducibilityAttrs.lean b/library/Init/Lean/ReducibilityAttrs.lean
index ebb3324e5e..eaf523708e 100644
--- a/library/Init/Lean/ReducibilityAttrs.lean
+++ b/library/Init/Lean/ReducibilityAttrs.lean
@@ -20,7 +20,7 @@ registerEnumAttributes `reducibility
    (`irreducible, "irreducible", ReducibilityStatus.irreducible)]
 
 @[init mkReducibilityAttrs]
-constant reducibilityAttrs : EnumAttributes ReducibilityStatus := default _
+constant reducibilityAttrs : EnumAttributes ReducibilityStatus := arbitrary _
 
 @[export lean_get_reducibility_status]
 def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus :=
diff --git a/library/Init/Lean/Runtime.lean b/library/Init/Lean/Runtime.lean
index 5878c49f39..27714be9a7 100644
--- a/library/Init/Lean/Runtime.lean
+++ b/library/Init/Lean/Runtime.lean
@@ -9,10 +9,10 @@ import Init.Core
 namespace Lean
 
 @[extern "lean_closure_max_args"]
-constant closureMaxArgsFn : Unit → Nat := default _
+constant closureMaxArgsFn : Unit → Nat := arbitrary _
 
 @[extern "lean_max_small_nat"]
-constant maxSmallNatFn : Unit → Nat := default _
+constant maxSmallNatFn : Unit → Nat := arbitrary _
 
 def closureMaxArgs : Nat :=
 closureMaxArgsFn ()
diff --git a/library/Init/Lean/Scopes.lean b/library/Init/Lean/Scopes.lean
index 1a0defa1a6..9c67595bd5 100644
--- a/library/Init/Lean/Scopes.lean
+++ b/library/Init/Lean/Scopes.lean
@@ -39,7 +39,7 @@ registerSimplePersistentEnvExtension {
 }
 
 @[init regScopeManagerExtension]
-constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := default _
+constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := arbitrary _
 
 namespace Environment
 
diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index 164f97bebb..6cd7a07621 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -27,7 +27,7 @@ instance TypedExpr.HasToString : HasToString TypedExpr :=
 ⟨λ ⟨val, type⟩ => "TypedExpr(" ++ toString val ++ ", " ++ toString type ++ ")"⟩
 
 instance TypedExpr.Inhabited : Inhabited TypedExpr :=
-⟨⟨default _, default _⟩⟩
+⟨⟨arbitrary _, arbitrary _⟩⟩
 
 structure Node : Type :=
 (anormSubgoal : Expr)
@@ -35,13 +35,13 @@ structure Node : Type :=
 (futureAnswer : TypedExpr)
 
 instance Node.Inhabited : Inhabited Node :=
-⟨⟨default _, {}, default _⟩⟩
+⟨⟨arbitrary _, {}, arbitrary _⟩⟩
 
 structure ConsumerNode extends Node :=
 (remainingSubgoals : List Expr)
 
 instance ConsumerNode.Inhabited : Inhabited ConsumerNode :=
-⟨⟨default _, default _⟩⟩
+⟨⟨arbitrary _, arbitrary _⟩⟩
 
 inductive Waiter : Type
 | consumerNode : ConsumerNode → Waiter
@@ -56,7 +56,7 @@ structure GeneratorNode extends Node :=
 (remainingInstances : List Instance)
 
 instance GeneratorNode.Inhabited : Inhabited GeneratorNode :=
-⟨⟨default _, default _⟩⟩
+⟨⟨arbitrary _, arbitrary _⟩⟩
 
 structure TableEntry : Type :=
 (waiters    : Array Waiter)
@@ -65,7 +65,7 @@ structure TableEntry : Type :=
 structure TCState : Type :=
 (env            : Environment)
 (finalAnswer    : Option TypedExpr                  := none)
-(mainMVar       : Expr                              := default _)
+(mainMVar       : Expr                              := arbitrary _)
 (generatorStack : Stack GeneratorNode               := Stack.empty)
 (consumerStack  : Stack ConsumerNode                := Stack.empty)
 (resumeQueue    : Queue (ConsumerNode × TypedExpr)  := Queue.empty)
diff --git a/library/Init/System/IO.lean b/library/Init/System/IO.lean
index e80787ca0b..a6b04631ae 100644
--- a/library/Init/System/IO.lean
+++ b/library/Init/System/IO.lean
@@ -60,10 +60,10 @@ match fn.run () with
 end
 
 @[extern "lean_io_timeit"]
-constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := default _
+constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitrary _
 
 @[extern "lean_io_allocprof"]
-constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := default _
+constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitrary _
 
 /- Programs can execute IO actions during initialization that occurs before
    the `main` function is executed. The attribute `[init <action>]` specifies
@@ -71,7 +71,7 @@ constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := default
 
    The action `initializing` returns `true` iff it is invoked during initialization. -/
 @[extern "lean_io_initializing"]
-constant IO.initializing : IO Bool := default _
+constant IO.initializing : IO Bool := arbitrary _
 
 abbrev monadIO (m : Type → Type) := HasMonadLiftT IO m
 
@@ -101,35 +101,35 @@ open Fs
   | Sum.inr b => pure b
 
 @[extern "lean_io_prim_put_str"]
-constant putStr (s: @& String) : IO Unit := default _
+constant putStr (s: @& String) : IO Unit := arbitrary _
 @[extern "lean_io_prim_read_text_file"]
-constant readTextFile (s : @& String) : IO String := default _
+constant readTextFile (s : @& String) : IO String := arbitrary _
 @[extern "lean_io_prim_get_line"]
-constant getLine : IO String := default _
+constant getLine : IO String := arbitrary _
 @[extern "lean_io_prim_handle_mk"]
-constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := default _
+constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := arbitrary _
 @[extern "lean_io_prim_handle_is_eof"]
-constant handle.isEof (h : @& handle) : IO Bool := default _
+constant handle.isEof (h : @& handle) : IO Bool := arbitrary _
 @[extern "lean_io_prim_handle_flush"]
-constant handle.flush (h : @& handle) : IO Unit := default _
+constant handle.flush (h : @& handle) : IO Unit := arbitrary _
 @[extern "lean_io_prim_handle_close"]
-constant handle.close (h : @& handle) : IO Unit := default _
+constant handle.close (h : @& handle) : IO Unit := arbitrary _
 -- TODO: replace `String` with byte buffer
 -- constant handle.read : handle → Nat → EIO String
 -- constant handle.write : handle → String → EIO Unit
 @[extern "lean_io_prim_handle_get_line"]
-constant handle.getLine (h : @& handle) : IO String := default _
+constant handle.getLine (h : @& handle) : IO String := arbitrary _
 
 @[extern "lean_io_getenv"]
-constant getEnv (var : @& String) : IO (Option String) := default _
+constant getEnv (var : @& String) : IO (Option String) := arbitrary _
 @[extern "lean_io_realpath"]
-constant realPath (fname : String) : IO String := default _
+constant realPath (fname : String) : IO String := arbitrary _
 @[extern "lean_io_is_dir"]
-constant isDir (fname : @& String) : IO Bool := default _
+constant isDir (fname : @& String) : IO Bool := arbitrary _
 @[extern "lean_io_file_exists"]
-constant fileExists (fname : @& String) : IO Bool := default _
+constant fileExists (fname : @& String) : IO Bool := arbitrary _
 @[extern "lean_io_app_dir"]
-constant appPath : IO String := default _
+constant appPath : IO String := arbitrary _
 
 @[inline] def liftIO {m : Type → Type} {α : Type} [monadIO m] (x : IO α) : m α :=
 monadLift x
@@ -235,21 +235,21 @@ end Proc
 
 
 /- References -/
-constant RefPointed (α : Type) : PointedType := default _
+constant RefPointed (α : Type) : PointedType := arbitrary _
 def Ref (α : Type) : Type := (RefPointed α).type
 instance (α : Type) : Inhabited (Ref α) := ⟨(RefPointed α).val⟩
 
 namespace Prim
 @[extern "lean_io_mk_ref"]
-constant mkRef {α : Type} (a : α) : IO (Ref α)                := default _
+constant mkRef {α : Type} (a : α) : IO (Ref α)                := arbitrary _
 @[extern "lean_io_ref_get"]
-constant Ref.get {α : Type} (r : @& Ref α) : IO α             := default _
+constant Ref.get {α : Type} (r : @& Ref α) : IO α             := arbitrary _
 @[extern "lean_io_ref_set"]
-constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit  := default _
+constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit  := arbitrary _
 @[extern "lean_io_ref_swap"]
-constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α     := default _
+constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α    := arbitrary _
 @[extern "lean_io_ref_reset"]
-constant Ref.reset {α : Type} (r : @& Ref α) : IO Unit         := default _
+constant Ref.reset {α : Type} (r : @& Ref α) : IO Unit        := arbitrary _
 end Prim
 
 section
diff --git a/library/Init/System/Platform.lean b/library/Init/System/Platform.lean
index 6f66784361..379b97e142 100644
--- a/library/Init/System/Platform.lean
+++ b/library/Init/System/Platform.lean
@@ -10,13 +10,13 @@ namespace System
 namespace Platform
 
 @[extern "lean_system_platform_nbits"]
-constant getNumBits : Unit → Nat := default _
+constant getNumBits : Unit → Nat := arbitrary _
 
 @[extern "lean_system_platform_windows"]
-constant getIsWindows : Unit → Bool := default _
+constant getIsWindows : Unit → Bool := arbitrary _
 
 @[extern "lean_system_platform_osx"]
-constant getIsOSX : Unit → Bool := default _
+constant getIsOSX : Unit → Bool := arbitrary _
 
 def numBits : Nat := getNumBits ()
 def isWindows : Bool := getIsWindows ()
diff --git a/library/Init/Util.lean b/library/Init/Util.lean
index 4dd120d9e8..aa23272aa3 100644
--- a/library/Init/Util.lean
+++ b/library/Init/Util.lean
@@ -23,10 +23,10 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α :=
 f ()
 
 @[extern c inline "#4"]
-unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := default _
+unsafe def unsafeCast {α : Type u} {β : Type v} [Inhabited β] (a : α) : β := arbitrary _
 
 @[neverExtract, extern c inline "lean_panic_fn(#3)"]
-constant panic {α : Type u} [Inhabited α] (msg : String) : α := default _
+constant panic {α : Type u} [Inhabited α] (msg : String) : α := arbitrary _
 
 @[neverExtract]
 def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=