chore(library/data/bitvec): remove leftover code
This commit is contained in:
parent
985c3697b9
commit
5bc5013f16
1 changed files with 0 additions and 7 deletions
|
|
@ -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}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue