mlkem: format properties correctly #147

Several properties didn't have correct `repl` commands in the docstrings.
GaloisInc · Oct 15, 2024 · cd05cb6 · cd05cb6
1 parent 50d8ab9
commit cd05cb6
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry
@@ -597,7 +597,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that NaiveNTT is self-inverting.
-         * ```
+         * ```repl
          * :prove NaiveNTT_Inverts
          * ```
          */
@@ -606,7 +606,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that NaiveNTTInv is self-inverting.
-         * ```
+         * ```repl
          * :prove NaiveNTTInv_Inverts
          * ```
          */
@@ -615,7 +615,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that `fast_ntt` is the inverse of `fast_invntt`.
-         * ```
+         * ```repl
          * :prove fast_ntt_inverts
          * ```
          */
@@ -624,7 +624,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that `fast_invntt` is the inverse of `fast_ntt`.
-         * ```
+         * ```repl
          * :prove fast_invntt_inverts
          * ```
          */
@@ -633,7 +633,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that `naive_ntt` is equivalent to `fast_ntt`.
-         * ```
+         * ```repl
          * :prove naive_fast_ntt_equiv
          * ```
          */
@@ -642,7 +642,7 @@ submodule NTT where
 
         /**
          * This property demonstrates that `naive_invntt` is equivalent to `fast_invntt`.
-         * ```
+         * ```repl
          * :prove naive_fast_invntt_equiv
          * ```
          */
@@ -709,7 +709,7 @@ MultiplyNTTs a b = join [BaseCaseMultiply (f_hat_i i) (g_hat_i i) (root i) | i :
     root i = (zeta^^(reverse (64 + (i >> 1)) >> 1) * ((-1 : (Z q)) ^^ (i)))
 
 /**
- * Testing that (1+x)^2 = 1+2x+x^2
+ * Testing that (1+x)^2 = 1+2x+x^2.
  * ```repl
  * :prove TestMult
  * ```