Working full proof, but incorrect/imprecise assumptions

AU-COBRA · Sep 4, 2024 · f49a446 · f49a446
1 parent a1faacd
commit f49a446
Show file tree

Hide file tree

Showing 2 changed files with 1,185 additions and 2,310 deletions.
diff --git a/theories/hacspec/Hacspec_ovn.v b/theories/hacspec/Hacspec_ovn.v
@@ -69,6 +69,7 @@ Module Type HacspecOvnParameter.
   Parameter (v_A_t_HasActions : t_HasActions v_A).
 
   Parameter (n : both uint_size).
+  Parameter (n_pos : Positive (is_pure n)).
 
   (* Extra from code *)
   Parameter (v_G_t_Sized : t_Sized v_G).