Add a test for the Field (Z p) instance.

Tracks the changes in Cryptol from GaloisInc/cryptol#882 which adds primality testing to the Cryptol type system, and implements field operations for `Z p`. Currently, we don't represent the primality test in SAWCore, but we might revisit this aspect in the future.
GaloisInc · Oct 8, 2020 · 4ef71a9 · 4ef71a9
1 parent 8f35e18
commit 4ef71a9
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/cryptol-saw-core/test/instance.cry b/cryptol-saw-core/test/instance.cry
@@ -188,6 +188,10 @@ fieldRational = recip
 fieldFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p
 fieldFloat = recip
 
+/* instance (prime p) => Field (Z p) */
+fieldZ : {p} prime p => Z p -> Z p
+fieldZ = recip
+
 ////////////////////////////////////////////////////////////////////////////////
 // Round