Skip to content

Commit

Permalink
Remove comment
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Sep 19, 2024
1 parent f6b2a58 commit 177d88d
Showing 1 changed file with 0 additions and 14 deletions.
14 changes: 0 additions & 14 deletions Arm/Insts/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -677,20 +677,6 @@ def shift_right_common_aux
shift_right_common_aux (e + 1) info operand operand2 result
termination_by (info.elements - e)


-- @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNatToHex : Lean.PrettyPrinter.Unexpander
-- | `($(_) $n:num $i:num) =>
-- let i' := i.getNat
-- let n' := n.getNat
-- let trimmed_hex := -- Remove leading zeroes...
-- String.dropWhile (BitVec.ofNat n' i').toHex
-- (fun c => c = '0')
-- -- ... but keep one if the literal is all zeros.
-- let trimmed_hex := if trimmed_hex.isEmpty then "0" else trimmed_hex
-- let bv := Lean.Syntax.mkNumLit s!"0x{trimmed_hex}#{n'}"
-- `($bv:num)
-- | _ => throw ()

-- FIXME: should this be upstreamed?
theorem shift_le (x : Nat) (shift :Nat) :
x >>> shift ≤ x := by
Expand Down

0 comments on commit 177d88d

Please sign in to comment.