Clean up binary representations and merkle trees (#22)

reilabs · Jan 28, 2024 · ae9327e · ae9327e
1 parent 1f19c61
commit ae9327e
Show file tree

Hide file tree

Showing 10 changed files with 688 additions and 1,497 deletions.
diff --git a/ProvenZk.lean b/ProvenZk.lean
@@ -2,10 +2,11 @@ import ProvenZk.Binary
 import ProvenZk.Gates
 import ProvenZk.Hash
 import ProvenZk.Merkle
+import ProvenZk.Ext.GetElem
 import ProvenZk.Ext.Vector
 import ProvenZk.Ext.Range
 import ProvenZk.Ext.Matrix
 import ProvenZk.Ext.List
 import ProvenZk.Ext.Fin
-import ProvenZk.Subvector
-import ProvenZk.Misc
+import ProvenZk.Lemmas
+import ProvenZk.UniqueAssignment