Skip to content

Commit

Permalink
Update src/Init/Data/BitVec/Bitblast.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Tobias Grosser <github@grosser.es>
  • Loading branch information
bollu and tobiasgrosser authored Sep 4, 2024
1 parent 1be4e45 commit 0cd3a29
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/Init/Data/BitVec/Bitblast.lean
Original file line number Diff line number Diff line change
Expand Up @@ -904,7 +904,6 @@ def divSubtractShiftProof (qr : ShiftSubtractInput w) (h : qr.Lawful wr wn n d)
have := h.hwn
omega


/- ### Core divsion recurrence.
We have three widths at play:
- w, the total bitwidth
Expand Down

0 comments on commit 0cd3a29

Please sign in to comment.