diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-08-26 16:50:48 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-08-26 16:50:48 -0700 |
| commit | d95707e8c3e8fa8ae58eeec15448556ab7eeb0b3 (patch) | |
| tree | 8dae527695e10f4f1123e56841258a6a6d718199 /src/Experiments | |
| parent | 7f918337e0ea4c05276ad2825873e9363fcf50e6 (diff) | |
Fix evalWordRangeOpt
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/SpecificCurve25519.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v index b5878825f..80f6ff3a6 100644 --- a/src/Experiments/SpecificCurve25519.v +++ b/src/Experiments/SpecificCurve25519.v @@ -118,6 +118,8 @@ Module Input. Definition ZInterp {t} E := @Interp Z ZEvaluable t E. + Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E. + Definition RangeInterp {n t} E: @interp_type (option (Range N)) t := typeMap evalWordRangeOpt (@Interp (@WordRangeOpt n) (@WordRangeOptEvaluable n) t E). |