diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index f73156faa9..cbbd884d13 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -145,13 +145,6 @@ section comparison end comparison -/- --- Create bitvecor from nat -def from_nat {n} : ℕ → bitvec n -| 0 := 0 -| (nat.succ x) := from_nat x + 1 --/ - section conversion variable {α : Type}