diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log new file mode 100644 index 000000000..c1012d128 --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log @@ -0,0 +1,25 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ, +Tbase Syntax.TZ x9 = x + x4; +Tbase Syntax.TZ x10 = x0 + x5; +Tbase Syntax.TZ x11 = x1 + x6; +Tbase Syntax.TZ x12 = x2 + x7; +Tbase Syntax.TZ x13 = x3 + x8; +(Return x9, Return x10, Return x11, Return x12, Return x13) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] |