Skip to content

Commit

Permalink
Remove ofBool, now that it is upstreamed to Std
Browse files Browse the repository at this point in the history
  • Loading branch information
alexkeizer committed Nov 17, 2023
1 parent 59c618e commit 8762730
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions Mathlib/Data/StdBitVec/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ comment them out for now.
### Structural
* `Std.BitVec.zeroExtendLE`: Zero extend a bitvector to a statically known larger size
* `Std.BitVec.ofBool`: Turn a Boolean into a bitvector of length 1
### Comparisons
* `Std.BitVec.sgt`: Signed greater-than comparison of bitvectors
Expand Down Expand Up @@ -95,11 +94,6 @@ namespace Std.BitVec
def zeroExtendLE {w v : ℕ} (h : w ≤ v) (x : BitVec w) : BitVec v :=
⟨x.toFin.castLE <| pow_le_pow (by decide) h⟩

/-- Turn a `Bool` into a bitvector of length `1` -/
def ofBool : Bool → BitVec 1
| true => 1
| false => 0

/-!
## Comparisons
-/
Expand Down

0 comments on commit 8762730

Please sign in to comment.