Significant generalization and extension of relations.

sandbox-quantum · Nov 6, 2024 · eb95c85 · eb95c85
1 parent e37ed39
commit eb95c85
Show file tree

Hide file tree

Showing 2 changed files with 539 additions and 131 deletions.
diff --git a/proofs/FO_KEM.eca b/proofs/FO_KEM.eca
@@ -18,5 +18,4 @@ type ctxt_t.
 
 
 (** Import basic PKE and KEM definitions **)
-clone import PublicKeyEncryption as PKE with
-  type pk_t <- 
+clone import PublicKeyEncryption as PKE.