diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-30 11:31:34 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-30 11:31:34 -0400 |
| commit | de1fac3d7fb19440931221b494902f5247279d77 (patch) | |
| tree | 2f05bd8db9ec6801b9d2102d5e350f240de8ff9b /src/Experiments/NewPipeline/AbstractInterpretationProofs.v | |
| parent | 6747dcc5532e83cf235693e1949262c8bf6ac7c0 (diff) | |
Generalize type.eqv a bit
Diffstat (limited to 'src/Experiments/NewPipeline/AbstractInterpretationProofs.v')
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index 60007288f..5c20da75b 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -51,7 +51,7 @@ Module Compilers. (Hwf : Wf E) (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) : forall arg1 arg2 - (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds E b_in)) arg1 = type.app_curried (Interp E) arg2. Proof. @@ -70,7 +70,7 @@ Module Compilers. (b_out : ZRange.type.base.option.interp (type.final_codomain t)) rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange E b_in b_out = inl rv) : forall arg1 arg2 - (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv _ _) arg1 arg2) + (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2) (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true), ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg1) = true /\ forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rv) arg1 |