chore: remove leftovers (#3537)
This commit is contained in:
parent
69e33efa2f
commit
e53ae5d89e
2 changed files with 0 additions and 4 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue