chore: fix tests

tests/compiler/lazylist.lean

@@ -36,7 +36,7 @@ partial def toList : LazyList α → List α
   | delayed as   => toList as.get
 
 partial def head [Inhabited α] : LazyList α → α
-  | nil          => arbitrary
+  | nil          => default
   | cons a as    => a
   | delayed as   => head as.get
 

tests/lean/run/536.lean

@@ -1,7 +1,7 @@
 variable (C : Type) [Inhabited C]
 
-example : C := arbitrary
+example : C := default
 
 variable {C}
 
-example : C := arbitrary
+example : C := default

tests/lean/run/def12.lean

@@ -2,7 +2,7 @@ def diag : Bool → Bool → Bool → Nat
 | b,  true, false => 1
 | false, b,  true => 2
 | true, false, b  => 3
-| b1, b2, b3 => arbitrary
+| b1, b2, b3 => default
 
 theorem diag1 (a : Bool) : diag a true false = 1 :=
 match a with
@@ -15,16 +15,16 @@ by cases a; exact rfl; exact rfl
 theorem diag3 (a : Bool) : diag true false a = 3 :=
 by cases a; exact rfl; exact rfl
 
-theorem diag4_1 : diag false false false = arbitrary :=
+theorem diag4_1 : diag false false false = default :=
 rfl
 
-theorem diag4_2 : diag true true true = arbitrary :=
+theorem diag4_2 : diag true true true = default :=
 rfl
 
 def f : Nat → Nat → Nat
 | n, 0 => 0
 | 0, n => 1
-| n, m => arbitrary
+| n, m => default
 
 theorem f_zero_right : (a : Nat) → f a 0 = 0
 | 0   => rfl
@@ -33,7 +33,7 @@ theorem f_zero_right : (a : Nat) → f a 0 = 0
 theorem f_zero_succ (a : Nat) : f 0 (a+1) = 1 :=
 rfl
 
-theorem f_succ_succ (a b : Nat) : f (a+1) (b+1) = arbitrary :=
+theorem f_succ_succ (a b : Nat) : f (a+1) (b+1) = default :=
 rfl
 
 def app {α} : List α → List α → List α

tests/lean/run/depElim1.lean

@@ -182,7 +182,7 @@ if worked then
   throwError "unexpected success"
 
 def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)
-:= arbitrary
+:= default
 
 #eval test `ex0 1 `elimTest0
 #print elimTest0
@@ -192,7 +192,7 @@ def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
 × LHS (forall (a : α) (as : List α) (b : β) (bs : List β), Pat (a::as) × Pat (b::bs))
 × LHS (forall (a : α) (as : List α), Pat (a::as) × Pat ([] : List β))
 × LHS (forall (b : β) (bs : List β), Pat ([] : List α) × Pat (b::bs))
-:= arbitrary
+:= default
 
 #eval test `ex1 2 `elimTest1
 
@@ -205,7 +205,7 @@ inductive Vec (α : Type u) : Nat → Type u
 def ex2 (α : Type u) (n : Nat) (xs : Vec α n) (ys : Vec α n) :
   LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0) × Pat (Vec.nil : Vec α 0))
 × LHS (forall (n : Nat) (x : α) (xs : Vec α n) (y : α) (ys : Vec α n), Pat (inaccessible (n+1)) × Pat (Vec.cons x xs) × Pat (Vec.cons y ys)) :=
-arbitrary
+default
 
 #eval test `ex2 3 `elimTest2
 #print elimTest2
@@ -215,7 +215,7 @@ def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
 × LHS (forall (a : α) (b : β), Pat [a] × Pat [b])
 × LHS (forall (a₁ a₂ : α) (as : List α) (b₁ b₂ : β) (bs : List β), Pat (a₁::a₂::as) × Pat (b₁::b₂::bs))
 × LHS (forall (as : List α) (bs : List β), Pat as × Pat bs)
-:= arbitrary
+:= default
 
 -- set_option trace.Meta.EqnCompiler.match true
 -- set_option trace.Meta.EqnCompiler.matchDebug true
@@ -226,7 +226,7 @@ def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) :
 def ex4 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0))
 × LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) :=
-arbitrary
+default
 
 #eval test `ex4 2 `elimTest4
 #print elimTest4
@@ -234,7 +234,7 @@ arbitrary
 def ex5 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0))
 × LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) :=
-arbitrary
+default
 
 #eval test `ex5 2 `elimTest5
 #print elimTest5
@@ -242,7 +242,7 @@ arbitrary
 def ex6 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (Pat (inaccessible Nat.zero) × Pat (Vec.nil : Vec α 0))
 × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary
+default
 
 -- set_option trace.Meta.Match.match true
 -- set_option trace.Meta.Match.debug true
@@ -253,7 +253,7 @@ arbitrary
 def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil))
 × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary
+default
 
 #eval test `ex7 2 `elimTest7
 -- #check elimTest7
@@ -275,7 +275,7 @@ elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none)
 def ex8 (α : Type u) (n : Nat) (xs : Vec α n) :
   LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil)))
 × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-arbitrary
+default
 
 #eval test `ex8 2 `elimTest8
 #print elimTest8
@@ -297,7 +297,7 @@ structure Node : Type :=
 def ex9 (xs : List Node) :
   LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
 × LHS (forall (ys : List Node), Pat ys) :=
-arbitrary
+default
 
 #eval test `ex9 1 `elimTest9
 #print elimTest9
@@ -319,14 +319,14 @@ inductive Foo : Bool → Prop
 def ex10 (x : Bool) (y : Foo x) :
   LHS (Pat (inaccessible false) × Pat Foo.bar)
 × LHS (forall (x : Bool) (y : Foo x), Pat (inaccessible x) × Pat y) :=
-arbitrary
+default
 
 #eval test `ex10 2 `elimTest10 true
 
 def ex11 (xs : List Node) :
   LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
 × LHS (Pat ([] : List Node)) :=
-arbitrary
+default
 
 #eval testFailure `ex11 1 `elimTest11 -- should produce error message
 
@@ -334,7 +334,7 @@ def ex12 (x y z : Bool) :
   LHS (forall (x y : Bool), Pat x × Pat y    × Pat true)
 × LHS (forall (x z : Bool), Pat false × Pat true × Pat z)
 × LHS (forall (y z : Bool), Pat true × Pat false × Pat z) :=
-arbitrary
+default
 
 #eval testFailure `ex12 3 `elimTest12 -- should produce error message
 
@@ -342,7 +342,7 @@ def ex13 (xs : List Node) :
   LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t))
 × LHS (forall (ys : List Node), Pat ys)
 × LHS (forall (ys : List Node), Pat ys) :=
-arbitrary
+default
 
 #eval testFailure `ex13 1 `elimTest13 -- should produce error message
 
@@ -350,7 +350,7 @@ def ex14 (x y : Nat) :
   LHS (Pat (val 1) × Pat (val 2))
 × LHS (Pat (val 2) × Pat (val 3))
 × LHS (forall (x y : Nat), Pat x × Pat y) :=
-arbitrary
+default
 
 -- set_option trace.Meta.Match true
 
@@ -370,7 +370,7 @@ def ex15 (xs : Array (List Nat)) :
   LHS (forall (a : Nat), Pat (ArrayLit1 [a]))
 × LHS (forall (a b : Nat), Pat (ArrayLit2 [a] [b]))
 × LHS (forall (ys : Array (List Nat)), Pat ys) :=
-arbitrary
+default
 
 #eval test `ex15 1 `elimTest15
 -- #check elimTest15
@@ -390,7 +390,7 @@ def ex16 (xs : List Nat) :
   LHS (forall (a : Nat) (xs : List Nat) (b : Nat) (as : List Nat), Pat (a :: As xs (b :: as)))
 × LHS (forall (a : Nat), Pat ([a]))
 × LHS (Pat ([] : List Nat)) :=
-arbitrary
+default
 
 #eval test `ex16 1 `elimTest16
 

tests/lean/run/fun.lean

@@ -1,15 +1,15 @@
 open Function Bool
 
 
-constant f : Nat → Bool := arbitrary
-constant g : Nat → Nat := arbitrary
+constant f : Nat → Bool := default
+constant g : Nat → Nat := default
 
 #check f ∘ g ∘ g
 
 #check (id : Nat → Nat)
 
-constant h : Nat → Bool → Nat := arbitrary
+constant h : Nat → Bool → Nat := default
 
 
-constant f1 : Nat → Nat → Bool := arbitrary
-constant f2 : Bool → Nat := arbitrary
+constant f1 : Nat → Nat → Bool := default
+constant f2 : Bool → Nat := default

tests/lean/run/methodsRetInhabited.lean

@@ -4,8 +4,8 @@ def exec (x : MacroM α) : Option α :=
   match x {
       mainModule := `Expander
       currMacroScope := 0
-      ref := arbitrary
-      methods := arbitrary } { macroScope := 0 } with
+      ref := default
+      methods := default } { macroScope := 0 } with
     | EStateM.Result.ok a s => a
     | _ => none
 

tests/lean/run/optParam.lean

@@ -8,10 +8,10 @@ theorem ex2 : (p (x := 1) |>.2) = 1 :=
 rfl
 
 def c {α : Type} [Inhabited α] : α × α :=
-(arbitrary, arbitrary)
+(default, default)
 
-theorem ex3 {α} [Inhabited α] : c.1 = arbitrary (α := α) :=
+theorem ex3 {α} [Inhabited α] : c.1 = default (α := α) :=
 rfl
 
-theorem ex4 {α} [Inhabited α] : c.2 = arbitrary (α := α) :=
+theorem ex4 {α} [Inhabited α] : c.2 = default (α := α) :=
 rfl

tests/lean/run/panicAtCheckAssignment.lean

@@ -5,7 +5,7 @@ open Lean.Meta
 
 def bug : MetaM Unit := do
   let i := 0
-  forallTelescopeReducing arbitrary fun ys _ => do
+  forallTelescopeReducing default fun ys _ => do
     let mut j := 0
     for y in ys do
       throwError "#{i+1}"

tests/lean/run/print_cmd.lean

@@ -1,4 +1,3 @@
-
 #print Nat
 
 private def foo (x : Nat) : Nat := x + 1
@@ -6,7 +5,7 @@ private def foo (x : Nat) : Nat := x + 1
 #print "hello"
 #print id
 #print propext
-#print arbitrary
+#print default
 #print ReaderT.read
 #print Prod
 #print Prod.mk

tests/lean/run/simp7.lean

@@ -26,7 +26,7 @@ theorem ex3 : fact x > 0 := by
     apply ih
 
 def head [Inhabited α] : List α → α
-  | []   => arbitrary
+  | []   => default
   | a::_ => a
 
 theorem ex4 [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=

tests/lean/run/simpMatchDiscr.lean

@@ -8,7 +8,7 @@ def Vec.repeat (a : α) (n : Nat) : Vec α n :=
   | n+1 => cons a (repeat a n)
 
 instance [Inhabited α] : Inhabited (Vec α n) where
-  default := Vec.repeat arbitrary n
+  default := Vec.repeat default n
 
 def Vec.map (v : Vec α n) (f : α → β) : Vec β n :=
   match n, v with

tests/lean/zipper.lean

@@ -23,7 +23,7 @@ def erase : ListZipper α → ListZipper α
 | ⟨x::xs, bs⟩ => ⟨xs, bs⟩
 
 def curr [Inhabited α] : ListZipper α → α
-| ⟨[], bs⟩    => arbitrary
+| ⟨[], bs⟩    => default
 | ⟨x::xs, bs⟩ => x
 
 def currOpt : ListZipper α → Option α