From 5bc5013f162ed256dd71d2beb0510a40de529f18 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@galois.com>
Date: Thu, 5 Jan 2017 23:55:34 -0800
Subject: [PATCH] chore(library/data/bitvec): remove leftover code

---
 library/data/bitvec.lean | 7 -------
 1 file changed, 7 deletions(-)

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}