aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log')
-rw-r--r--src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log14
1 files changed, 1 insertions, 13 deletions
diff --git a/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log b/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log
index 73c0717f8..eb0b6ea33 100644
--- a/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log
+++ b/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log
@@ -19,16 +19,4 @@ Interp-η
uint32_t x45 = (x2 | x44);
return x45)
x
- : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in
- lower) with
- | 0%Z => Eq
- | Z.pos _ => Lt
- | Z.neg _ => Gt
- end with
- | Eq => true
- | Lt => true
- | Gt => false
- end then Some 5 else None) with
- | Some lgsz => Syntax.TWord lgsz
- | None => Syntax.TZ
- end)
+ : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t