diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-10-10 14:58:34 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-10-10 14:58:36 -0400 |
| commit | 7c28d4f8f6566a01dcf1cdbb5610f68a9bf23661 (patch) | |
| tree | 32055482ddfd4e8ac969e6fa05ae6c96c6db2c44 /src/Util/Tuple.v | |
| parent | a75c0c7dd83e2b1b92784b4d5d7a222f6fe9bc52 (diff) | |
Ed25519: add basepoint and prove most EdDSA preconditions
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 6ef7a0ca4..bcfc7be5b 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -142,12 +142,12 @@ Proof. { exact _. } { intros ??. exact _. } -Qed. +Defined. Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10. Proof. destruct n; unfold fieldwise; exact _. -Qed. +Defined. Fixpoint fieldwiseb' {A B} (n:nat) (R:A->B->bool) (a:tuple' A n) (b:tuple' B n) {struct n} : bool. destruct n; simpl @tuple' in *. |