diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 3430622733..bd1ad69203 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -666,9 +666,6 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁) (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl)) -#print get -#print set - @[simp] theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} : (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl diff --git a/src/Lean/Meta/LitValues.lean b/src/Lean/Meta/LitValues.lean index f64ca4252c..319814c896 100644 --- a/src/Lean/Meta/LitValues.lean +++ b/src/Lean/Meta/LitValues.lean @@ -78,7 +78,6 @@ def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := Optio let v ← getNatValue? (e.getArg!' 1) return ⟨n, BitVec.ofNat n v⟩ let (v, type) ← getOfNatValue? e ``BitVec - IO.println v let n ← getNatValue? (← whnfD type.appArg!) return ⟨n, BitVec.ofNat n v⟩