diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-17 14:39:18 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-17 14:39:18 -0700 |
| commit | f8680ec8e73f8acb39cb55f6e616a0e5d10347f8 (patch) | |
| tree | d13ad67b22fcce1dd72946d3aef2532e785ef9ac /src/Assembly/HL.v | |
| parent | 075347c125e6bdb77c1e0f4ed229d5019b213584 (diff) | |
Converting to bounded machinery
Diffstat (limited to 'src/Assembly/HL.v')
| -rw-r--r-- | src/Assembly/HL.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v index 9f8ff27bd..264cd0351 100644 --- a/src/Assembly/HL.v +++ b/src/Assembly/HL.v @@ -49,12 +49,6 @@ Module HL. Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E. - Definition rangeInterp {n t} E: @interp_type (option (Range N)) t := - typeMap rangeEval (@interp (@WordRangeOpt n) (@WordRangeOptEvaluable n) t E). - - Definition RangeInterp {n t} E: @interp_type (option (Range N)) t := - typeMap rangeEval (@Interp (@WordRangeOpt n) (@WordRangeOptEvaluable n) t E). - Example example_Expr : Expr TT := fun var => ( Let (Const 7) (fun a => Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p => |