diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 15:13:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 15:13:43 -0400 |
| commit | 6d3772435f9924df0984c8050766b154d7c41f8d (patch) | |
| tree | 7d969faa3629be9bb225274f31247137209981c5 /src/Specific/GF25519.v | |
| parent | 549d05f1105340952ef9075381ae5fb5f3bffe13 (diff) | |
Add {un,}curry_wire_digits
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 6f870e8da..a39755eee 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -184,6 +184,11 @@ Definition uncurry_binop_fe25519 {T} (op : fe25519 -> fe25519 -> T) Definition curry_binop_fe25519 {T} op : fe25519 -> fe25519 -> T := Eval compute in appify2 (fun f => curry_unop_fe25519 (curry_unop_fe25519 op f)). +Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) + := Eval compute in Tuple.uncurry (n:=length wire_widths) op. +Definition curry_unop_wire_digits {T} op : wire_digits -> T + := Eval compute in fun f => app_7 f (Tuple.curry (n:=length wire_widths) op). + Definition add_sig (f g : fe25519) : { fg : fe25519 | fg = add_opt f g}. Proof. |