chore: update to nightly-testing-2024-12-20 (#906)

SSA/Core/Util.lean

@@ -94,13 +94,13 @@ elab "print_goal_as_error " : tactic => do
   pure ()
 
 -- TODO: should these go into Std?
-def Vector.ofList {α : Type u} (l : List α) : Mathlib.Vector α l.length :=
+def Vector.ofList {α : Type u} (l : List α) : List.Vector α l.length :=
 ⟨l, rfl⟩
 
-def Vector.ofArray {α : Type u} (a : Array α) : Mathlib.Vector α a.size :=
+def Vector.ofArray {α : Type u} (a : Array α) : List.Vector α a.size :=
  Vector.ofList a.toList
 
-instance [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (Mathlib.Vector τ n) where
+instance [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (List.Vector τ n) where
   name := s!"Vector ({inst.name}) {n}"
   parse? str := do
     let arr : Array τ ← Cli.ParseableType.parse? str

SSA/Core/Util/ConcreteOrMVar.lean

@@ -44,7 +44,7 @@ def instantiateOne (a : α) : ConcreteOrMVar α (φ+1) → ConcreteOrMVar α φ
       (fun j => .mvar j)  -- `i = Fin.castSucc j`
 
 /-- Instantiate all meta-variables -/
-def instantiate (as : Mathlib.Vector α φ) : ConcreteOrMVar α φ → α
+def instantiate (as : List.Vector α φ) : ConcreteOrMVar α φ → α
   | .concrete w => w
   | .mvar i => as.get i
 
@@ -54,14 +54,14 @@ def ofNat_eq_concrete (x : Nat) :
     (OfNat.ofNat x) = (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) := rfl
 
 @[simp]
-def instantiate_ofNat_eq (as : Mathlib.Vector Nat φ) (x : Nat) :
+def instantiate_ofNat_eq (as : List.Vector Nat φ) (x : Nat) :
    ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl
 
 @[simp]
 lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} :
     ConcreteOrMVar.instantiate (Subtype.mk (w :: ws) hφ)  (ConcreteOrMVar.mvar ⟨0, h0⟩) = w := by
   simp [instantiate]
-  simp [Mathlib.Vector.get]
+  simp [List.Vector.get]
 
 @[simp]
 lemma instantiate_mvar_zero' :

SSA/Experimental/Bits/AutoStructs/Defs.lean

@@ -328,7 +328,7 @@ def Formula.language (φ : Formula) : Set (BitVecs φ.arity) :=
     l'.proj fun n => n.castLE (by simp [Formula.arity, FinEnum.card])
 
 lemma helper1 : (k = 0) → (x ::ᵥ vs).get k = x := by rintro rfl; simp
-lemma helper2 : (k = 1) → (x ::ᵥ y ::ᵥ vs).get k = y := by rintro rfl; simp [Mathlib.Vector.get]
+lemma helper2 : (k = 1) → (x ::ᵥ y ::ᵥ vs).get k = y := by rintro rfl; simp [List.Vector.get]
 lemma msb_coe {x : BitVec w1} (heq : w1 = w2) : x.msb = (heq ▸ x).msb := by rcases heq; simp
 
 lemma formula_language_case_atom :
@@ -356,7 +356,7 @@ lemma formula_language_case_atom :
       apply hrel
     have ht1 : bvsb.bvs.get n = t1.evalFin fun n => bvsb.bvs.get n := by
       unfold Term.language at h1
-      simp [Mathlib.Vector.transport, liftMaxSucc1] at h1
+      simp [List.Vector.transport, liftMaxSucc1] at h1
       unfold n; simp +zetaDelta; rw [←h1]
       congr; ext1 k
       split_ifs with h
@@ -367,7 +367,7 @@ lemma formula_language_case_atom :
       · congr; ext; simp; rw [Nat.mod_eq_of_lt]; omega
     have ht2 : bvsb.bvs.get (Fin.last (n+1)) = t2.evalFin fun n => bvsb.bvs.get n := by
       unfold Term.language at h2
-      simp [Mathlib.Vector.transport, liftMaxSucc2] at h2
+      simp [List.Vector.transport, liftMaxSucc2] at h2
       unfold n; simp +zetaDelta only [Formula.arity, Fin.natCast_self]; rw [←h2]
       congr; ext1 k
       split_ifs with h
@@ -382,14 +382,14 @@ lemma formula_language_case_atom :
       apply evalFin_eq hw; intros k
       rcases bvs with ⟨w, bvs⟩; rcases hw
       injection heqb with _ heqb; rw [←heqb]
-      simp [Mathlib.Vector.transport, liftExcept2]
+      simp [List.Vector.transport, liftExcept2]
       congr; ext; simp; omega
     have heq2 : (t2.evalFin fun n => bvsb.bvs.get n) =
         hw ▸ t2.evalFin fun n => bvs.bvs.get $ n.castLE (by simp) := by
       apply evalFin_eq hw; intros k
       rcases bvs with ⟨w, bvs⟩; rcases hw
       injection heqb with _ heqb; rw [←heqb]
-      simp [Mathlib.Vector.transport, liftExcept2]
+      simp [List.Vector.transport, liftExcept2]
       congr; ext; simp; omega
     rw [ht1, ht2, heq1, heq2, evalRelation_coe] at hrel
     dsimp only [Set.instMembership, Set.Mem]
@@ -398,21 +398,21 @@ lemma formula_language_case_atom :
     simp
     let bv1 := t1.evalFin fun k => bvs.bvs.get $ k.castLE (by simp)
     let bv2 := t2.evalFin fun k => bvs.bvs.get $ k.castLE (by simp)
-    use ⟨bvs.w, bvs.bvs.append $ bv1 ::ᵥ bv2 ::ᵥ Mathlib.Vector.nil⟩
+    use ⟨bvs.w, bvs.bvs.append $ bv1 ::ᵥ bv2 ::ᵥ List.Vector.nil⟩
     rcases bvs with ⟨w, bvs⟩
     simp
     constructor
     · unfold l; simp; split_ands
       · unfold lrel; simp only [Fin.isValue, BitVecs.transport_getElem,
           liftLast2, Set.mem_setOf_eq, Fin.val_last, le_add_iff_nonneg_right, zero_le,
-          Mathlib.Vector.append_get_ge]
-        rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)]
+          List.Vector.append_get_ge]
+        rw [List.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)]
         simp [Set.instMembership, Set.Mem] at h
         convert h using 2
         · apply helper1; ext; simp; rw [Nat.mod_eq_of_lt] <;> omega
         · apply helper2; ext; simp
-      · unfold l1 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc1]
-        rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)]
+      · unfold l1 Term.language; simp [List.Vector.transport, liftMaxSucc1]
+        rw [List.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)]
         rw [helper1 (by ext; simp; rw [Nat.mod_eq_of_lt] <;> omega)]
         unfold bv1
         congr; ext1 k; split_ifs
@@ -421,7 +421,7 @@ lemma formula_language_case_atom :
           have _ : k = t1.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last]
           omega
         · simp; congr 1
-      · unfold l2 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc2]
+      · unfold l2 Term.language; simp [List.Vector.transport, liftMaxSucc2]
         rw [helper2 (by ext; simp)]
         unfold bv2
         congr; ext1 k; split_ifs
@@ -432,8 +432,8 @@ lemma formula_language_case_atom :
         · simp; congr 1
     · ext1; simp
       next i =>
-        simp [Mathlib.Vector.transport, liftExcept2]
-        rw [Mathlib.Vector.append_get_lt i.isLt]
+        simp [List.Vector.transport, liftExcept2]
+        rw [List.Vector.append_get_lt i.isLt]
         congr 1
 
 theorem formula_language (φ : Formula) :
@@ -456,7 +456,7 @@ theorem formula_language (φ : Formula) :
       congr!
     rcases op <;>
       simp [evalBinop, langBinop, Set.compl, Set.instMembership,
-        Set.Mem, Mathlib.Vector.transport] <;> simp_all <;> tauto
+        Set.Mem, List.Vector.transport] <;> simp_all <;> tauto
   case msbSet t =>
     ext1 bvs; simp only [Formula.arity, Formula.language, Set.proj, Set.lift, langMsb, Fin.isValue,
       Set.preimage_setOf_eq, Set.mem_image, Set.mem_inter_iff,
@@ -466,19 +466,19 @@ theorem formula_language (φ : Formula) :
     · rintro ⟨bvsb, ⟨ht, hmsb⟩, heq⟩
       simp only [Fin.isValue, Formula.arity] at ht hmsb ⊢
       unfold Term.language at ht
-      simp only [BitVecs.transport, Mathlib.Vector.transport] at hmsb
+      simp only [BitVecs.transport, List.Vector.transport] at hmsb
       simp at ht; rw [←ht] at hmsb; rw [←hmsb]
       simp [BitVecs.transport] at heq
       obtain ⟨hw, hbvs⟩ := heq
       simp [hw]; congr 1; simp [hw]
       rcases hw; simp
       congr 1; ext1 k
-      simp at hbvs; simp [←hbvs, Mathlib.Vector.transport]; congr
+      simp at hbvs; simp [←hbvs, List.Vector.transport]; congr
     · intros heq
       use ⟨w,
-        bvs.append ((t.evalFin fun k => bvs.get $ k.castLE (by simp)) ::ᵥ Mathlib.Vector.nil)⟩
+        bvs.append ((t.evalFin fun k => bvs.get $ k.castLE (by simp)) ::ᵥ List.Vector.nil)⟩
       unfold Term.language
-      simp [BitVecs.transport, Mathlib.Vector.transport] at heq ⊢
+      simp [BitVecs.transport, List.Vector.transport] at heq ⊢
       constructor; assumption
       ext1 k; simp; congr 1
 
@@ -527,7 +527,7 @@ lemma sat_impl_sat' {φ : Formula} :
     simp [←evalFin_evalNat]
 
 lemma env_to_bvs (φ : Formula) (ρ : Fin φ.arity → BitVec w) :
-    let bvs : BitVecs φ.arity := ⟨w, Mathlib.Vector.ofFn fun k => ρ k⟩
+    let bvs : BitVecs φ.arity := ⟨w, List.Vector.ofFn fun k => ρ k⟩
     ρ = fun k => bvs.bvs.get k := by
   simp
 

SSA/Experimental/Bits/AutoStructs/ForLean.lean

@@ -39,10 +39,6 @@ theorem Array.take_ge_size {a : Array α} {n} (h : n ≥ a.size) : a.take n = a
   have heq : a.size - n = 0 := by omega
   rw [heq]; rfl
 
-@[simp]
-theorem Array.take_size {a : Array α} : a.take a.size = a :=
-  a.take_ge_size (Nat.le_refl a.size)
-
 @[simp]
 theorem Array.take_zero {a : Array α} : a.take 0 = #[] := eq_empty_of_size_eq_zero (by simp)
 

SSA/Experimental/Bits/AutoStructs/ForMathlib.lean

@@ -11,17 +11,17 @@ open Set
 open Mathlib
 
 @[simp]
-lemma Mathlib.Vector.append_get_lt {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: i < n) :
+lemma List.Vector.append_get_lt {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: i < n) :
     (x.append y).get i = x.get (i.castLT hlt) := by
   rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩
-  dsimp [Mathlib.Vector.append, Mathlib.Vector.get]
+  dsimp [List.Vector.append, List.Vector.get]
   apply List.getElem_append_left
 
 @[simp]
-lemma Mathlib.Vector.append_get_ge {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) :
+lemma List.Vector.append_get_ge {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) :
     (x.append y).get i = y.get ((i.cast (Nat.add_comm n m) |>.subNat n hlt)) := by
   rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩
-  dsimp [Mathlib.Vector.append, Mathlib.Vector.get]
+  dsimp [List.Vector.append, List.Vector.get]
   rcases hx
   apply List.getElem_append_right hlt
 
@@ -40,7 +40,7 @@ instance finenum_fin : FinEnum (Fin n) where
 instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
 instance (α : Type) : Union (Language α) := ⟨Set.union⟩
 
-def Mathlib.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n :=
+def List.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n :=
   Vector.ofFn fun i => v.get (f i)
 
 def BitVec.transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 :=
@@ -63,14 +63,14 @@ The set of `n`-tuples of bit vectors of an arbitrary width.
 -/
 structure BitVecs (n : Nat) where
   w : Nat
-  bvs : Mathlib.Vector (BitVec w) n
+  bvs : List.Vector (BitVec w) n
 
-abbrev BitVecs.empty : BitVecs n := ⟨0, Mathlib.Vector.replicate n .nil⟩
+abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
 abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
 abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩
 
 def BitVecs0 : Set (BitVecs n) :=
-  {⟨0, Vector.replicate n (BitVec.zero 0)⟩}
+  {⟨0, List.Vector.replicate n (BitVec.zero 0)⟩}
 
 -- TODO: this ought to be way easier
 @[ext (iff := false)]
@@ -100,7 +100,7 @@ def enc (bvs : BitVecs n) : BitVecs' n :=
 
 def dec (bvs' : BitVecs' n) : BitVecs n where
   w := bvs'.length
-  bvs := Mathlib.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k
+  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k
 
 @[simp]
 lemma dec_nil n : dec (n := n) [] = BitVecs.empty := by
@@ -142,7 +142,7 @@ lemma dec_enc : Function.RightInverse (α := BitVecs' n) enc dec := by
   intros bvs; ext1; exact dec_enc_w bvs
   next i =>
     simp only [enc, Fin.getElem_fin, dec, List.getElem_map, List.getElem_finRange, Fin.cast_mk,
-      Fin.is_lt, BitVec.ofFn_getLsbD', Fin.eta, Vector.get_ofFn]
+      Fin.is_lt, BitVec.ofFn_getLsbD', Fin.eta, List.Vector.get_ofFn]
     ext
     simp_all only [List.length_map, List.length_finRange, BitVec.ofFn_getLsbD',
       BitVec.getLsbD_cast']
@@ -177,9 +177,9 @@ def dec_inj {n : Nat} : Function.Injective (dec (n := n)) := by
 @[simp]
 lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) : dec (bvs' ++ [a]) =
   { w := bvs'.length + 1
-    bvs := Mathlib.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } := by
+    bvs := List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } := by
   ext k i <;> simp_all only [dec, Fin.getElem_fin, List.length_append, List.length_singleton,
-    Vector.get_ofFn, BitVec.ofFn_getLsbD', BitVec.getLsbD_cast']
+    List.Vector.get_ofFn, BitVec.ofFn_getLsbD', BitVec.getLsbD_cast']
   rw [BitVec.getLsbD_cons]
   split
   next heq => simp_all
@@ -204,7 +204,7 @@ lemma BitVecs.transport_w {bvs : BitVecs n} : (BitVecs.transport f bvs).w = bvs.
 @[simp]
 lemma BitVecs.transport_getElem {bvs : BitVecs m} (f : Fin n → Fin m) (i : Fin n) :
     (bvs.transport f).bvs.get i = bvs.bvs.get (f i) := by
-  simp [transport, Mathlib.Vector.transport]
+  simp [transport, List.Vector.transport]
 
 def BitVecs'.transport (f : Fin n → Fin m) (bvs' : BitVecs' m): BitVecs' n :=
   bvs'.map fun bv => bv.transport f

SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean

@@ -38,7 +38,7 @@ lemma NFA.correct_spec {M : NFA α σ} {ζ : M.sa} {L : Language α} :
   simp_all
 
 abbrev BVRel := ∀ ⦃w⦄, BitVec w → BitVec w → Prop
-abbrev BVNRel n := ∀ ⦃w⦄, Mathlib.Vector (BitVec w) n → Prop
+abbrev BVNRel n := ∀ ⦃w⦄, List.Vector (BitVec w) n → Prop
 
 def NFA'.sa (M : NFA' n) := M.σ → BVNRel n
 def NFA'.sa2 (M : NFA' 2) := M.σ → BVRel
@@ -56,7 +56,7 @@ lemma in_enc : x ∈ enc '' S ↔ dec x ∈ S := by
   · rintro hS; use dec x; simp_all
 
 @[simp]
-lemma Mathlib.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by
+lemma List.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by
   simp [ofFn]
 
 @[simp]
@@ -66,7 +66,7 @@ lemma BitVec.ofFn_0 {f : Fin 0 → Bool} : ofFn f = .nil := by
 @[simp]
 lemma dec_snoc_in_langRel {n} {R : BVNRel n} {w : BitVecs' n} {a : BitVec n} :
     dec (w ++ [a]) ∈ langRel R ↔
-      R (Mathlib.Vector.ofFn fun k => .cons (a.getLsbD k) ((dec w).bvs.get k)) := by
+      R (List.Vector.ofFn fun k => .cons (a.getLsbD k) ((dec w).bvs.get k)) := by
   simp [langRel]
 
 @[simp]
@@ -117,10 +117,10 @@ lemma BitVec.cons_inj : cons b1 bv1 = cons b2 bv2 ↔ (b1 = b2) ∧ bv1 = bv2 :=
 @[simp] lemma BitVec.lk01 : (0#2 : BitVec 2)[1] = false := by rfl
 
 structure NFA'.correct (M : NFA' n) (ζ : M.sa) (L : BVNRel n) where
-  cond1 : ∀ ⦃w⦄ (bvn : Mathlib.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn)
-  cond2 q : q ∈ M.M.start ↔ ζ q (Vector.replicate n .nil)
-  cond3 q a {w} (bvn : Mathlib.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔
-              ζ q (Mathlib.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k))
+  cond1 : ∀ ⦃w⦄ (bvn : List.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn)
+  cond2 q : q ∈ M.M.start ↔ ζ q (List.Vector.replicate n .nil)
+  cond3 q a {w} (bvn : List.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔
+              ζ q (List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k))
 
 structure NFA'.correct2 (M : NFA' 2) (ζ : M.sa2) (L : BVRel) where
   cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2)
@@ -155,7 +155,7 @@ lemma NFA'.correct_spec {M : NFA' n} {ζ : M.sa} {L : BVNRel n} :
 lemma NFA'.correct2_spec {M : NFA' 2} {ζ : M.sa2} {L : BVRel} :
     M.correct2 ζ L → M.accepts = langRel2 L := by
   rintro ⟨h1, h2, h3⟩
-  suffices hc : M.correct (fun q w (bvn : Mathlib.Vector (BitVec w) 2) => ζ q (bvn.get 0) (bvn.get 1))
+  suffices hc : M.correct (fun q w (bvn : List.Vector (BitVec w) 2) => ζ q (bvn.get 0) (bvn.get 1))
                       (fun w bvn => L (bvn.get 0) (bvn.get 1)) by
     rw [M.correct_spec hc]
     simp [langRel2, langRel]
@@ -188,7 +188,7 @@ def _root_.NFA'.ofFSM'  (p : FSM arity) : NFA' (FinEnum.card arity + 1) where
   M := NFA.ofFSM p
 
 @[simp]
-abbrev inFSMRel (p : FSM arity) {w} (bvn : Mathlib.Vector (BitVec w) _) :=
+abbrev inFSMRel (p : FSM arity) {w} (bvn : List.Vector (BitVec w) _) :=
   bvn.get (Fin.last (FinEnum.card arity)) = p.evalBV (fun ar => bvn.get (FinEnum.equiv.toFun ar))
 
 def NFA'.ofFSM_sa (p : FSM arity) : (NFA'.ofFSM' p).sa := fun q _ bvn =>
@@ -343,7 +343,7 @@ lemma evalFinStream_evalFin {t : Term} {k : Nat} (hlt : k < w) (vars : Fin t.ari
     symm; apply BitStream.neg_congr; simp_all
 
 @[simp]
-lemma FSM.eval_bv (bvn : Mathlib.Vector (BitVec w) (t.arity + 1)) :
+lemma FSM.eval_bv (bvn : List.Vector (BitVec w) (t.arity + 1)) :
   ((FSM.ofTerm t).evalBV fun ar => bvn.get ar.castSucc) =
     (t.evalFin fun ar => bvn.get ar.castSucc) := by
   simp [FSM.evalBV]; ext k hk

SSA/Projects/InstCombine/Base.lean

@@ -284,7 +284,7 @@ instance : ToString (MOp φ) where
 
 abbrev Op := MOp 0
 
-def MOp.UnaryOp.instantiate (as : Mathlib.Vector Nat φ) : MOp.UnaryOp φ → MOp.UnaryOp 0
+def MOp.UnaryOp.instantiate (as : List.Vector Nat φ) : MOp.UnaryOp φ → MOp.UnaryOp 0
 | .trunc w' flags     => .trunc (.concrete <| w'.instantiate as) flags
 | .zext w' flag => .zext (.concrete <| w'.instantiate as) flag
 | .sext w'      => .sext (.concrete <| w'.instantiate as)

SSA/Projects/InstCombine/LLVM/CLITests.lean

@@ -201,11 +201,11 @@ def CliTest.eval (test : CliTest) (values : Vector ℤ test.context.length)
 -/
 
 def InstCombine.mkValuation (ctxt : MContext 0)
-  (values : Mathlib.Vector (Option Int) ctxt.length): Ctxt.Valuation ctxt :=
+  (values : List.Vector (Option Int) ctxt.length): Ctxt.Valuation ctxt :=
 match ctxt, values with
   | [], ⟨[],_⟩ => Ctxt.Valuation.nil
   | ty::tys, ⟨val::vals,hlen⟩ =>
-    let valsVec : Mathlib.Vector (Option Int) tys.length := ⟨vals,by aesop⟩
+    let valsVec : List.Vector (Option Int) tys.length := ⟨vals,by aesop⟩
     let valuation' := mkValuation tys valsVec
     match ty with
       | .bitvec (.concrete w) =>
@@ -214,7 +214,7 @@ match ctxt, values with
          Ctxt.Valuation.snoc valuation' newTy
 
 def ConcreteCliTest.eval (test : ConcreteCliTest)
-    (values : Mathlib.Vector (Option Int) test.context.length) :
+    (values : List.Vector (Option Int) test.context.length) :
  IO ⟦test.ty⟧ := do
   let valuesStack := values.reverse -- we reverse values since context is a stack
   let valuation := InstCombine.mkValuation test.context valuesStack
@@ -223,14 +223,14 @@ def ConcreteCliTest.eval (test : ConcreteCliTest)
 def ConcreteCliTest.eval? (test : ConcreteCliTest) (values : Array (Option Int)) :
   IO (Except String ⟦test.ty⟧) := do
     if h : values.size = test.context.length then
-      let valuesVec : Mathlib.Vector (Option Int) test.context.length := h ▸ (Vector.ofArray values)
+      let valuesVec : List.Vector (Option Int) test.context.length := h ▸ (Vector.ofArray values)
       return Except.ok <| (← test.eval valuesVec)
     else
       return Except.error (s!"Invalid input length: {values} has length {values.size}, " ++
         s!" required {test.context.length}")
 
 def ConcreteCliTest.parseableInputs (test : ConcreteCliTest) :
-    Cli.ParseableType (Mathlib.Vector Int test.context.length)
+    Cli.ParseableType (List.Vector Int test.context.length)
   := inferInstance
 
 def CocreteCliTest.signature (test : ConcreteCliTest) :