aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log
blob: e9a2afeb3c9a37634dbe558b1c9abb0f5c0f327e (plain)
1
2
3
4
5
6
7
8
λ x : word128 * word128,
Interp-η
(λ var : Syntax.base_type → Type,
 λ '(x1, x2)%core,
 uint128_t x3 = x2 | x1;
 return x3)
x
     : word128 * word128 → ReturnType uint128_t