clean

Author: osmanyasar05

DatapathVerification/BitHeap/BitHeap.lean

@@ -29,11 +29,7 @@ structure AdderResult where
   carry : Circuit
 
 def removeBit (column : Nat) (c : Circuit) (h : BitHeap) : BitHeap :=
-  ⟨h.columns.modify column (fun col => ⟨col.elems.erase c⟩)⟩
-
-def columnsWithFrom (column : Nat) (c : Circuit) (h : BitHeap) : Nat :=
-  h.columns.fold (fun acc k col =>
-    if k ≥ column && col.contains c then acc + 1 else acc) 0
+  ⟨h.columns.modify column (fun col => col.erase c)⟩
 
 /--
 Add a bit into the bit heap, returning a new bit heap. If the bit already exists in the column, remove it and add it to the next column.

DatapathVerification/BitHeap/Column.lean

@@ -14,17 +14,21 @@ deriving Inhabited, Repr
 
 namespace Column
 
+def contains (col : Column) (c : Circuit) : Bool :=
+  col.elems.contains c
+
 def empty : Column := ⟨Std.HashSet.emptyWithCapacity 0⟩
 
+def eval (col : Column) (env : BitEnv) : Nat :=
+  (col.elems.fold (init := 0) (fun acc (c : Circuit) => acc + (c.eval env).toNat))
+
 def insert (col : Column) (c : Circuit) : Column :=
   let col := ⟨col.elems.insert c⟩
   col
 
-def contains (col : Column) (c : Circuit) : Bool :=
-  col.elems.contains c
-
-def eval (col : Column) (env : BitEnv) : Nat :=
-  (col.elems.fold (init := 0) (fun acc (c : Circuit) => acc + (c.eval env).toNat))
+def erase (col : Column) (c : Circuit) : Column :=
+  let col := ⟨col.elems.erase c⟩
+  col
 
 end Column