diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 19:37:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 19:37:39 -0400 |
| commit | a59409711a52436ac92f0e3aa149bba5ac81c996 (patch) | |
| tree | a00d78e6500a391bc5d2fea40827608dcb913a76 /src/Reflection | |
| parent | 260dca24d6a1b517cd90932f4c57519e6bf8e0eb (diff) | |
Add InterpExprEta_arrow
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/EtaInterp.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v index 52e816df5..170056a02 100644 --- a/src/Reflection/EtaInterp.v +++ b/src/Reflection/EtaInterp.v @@ -87,4 +87,10 @@ Section language. Lemma InterpExprEta' {t e} : forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x. Proof. apply interp_expr_eta'. Qed. + Lemma InterpExprEta_arrow {s d e} + : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x = Interp (@interp_op) e x. + Proof. exact (@InterpExprEta (Arrow s d) e). Qed. + Lemma InterpExprEta'_arrow {s d e} + : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x. + Proof. exact (@InterpExprEta' (Arrow s d) e). Qed. End language. |