diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 19:41:10 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 19:41:10 -0400 |
| commit | e04a4621687b2d22d6ea7211b3679f1f6a1cbce8 (patch) | |
| tree | dd50adadca97a83f6b9d71dbf61f401f2b7d6a39 /src/Reflection | |
| parent | a59409711a52436ac92f0e3aa149bba5ac81c996 (diff) | |
Add Wf_MapCast_arrow
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index eebd1330d..2cb7e2f40 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -98,6 +98,15 @@ Section language. try solve [ auto using name_list_unique_DefaultNamesFor | intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence ]. Qed. + + Lemma Wf_MapCast_arrow + {s d} (e : Expr base_type_code op (Arrow s d)) + (Hwf : Wf e) + (input_bounds : interp_flat_type interp_base_type_bounds s) + : forall {b} (e' : Expr _ _ (Arrow (pick_type input_bounds) (pick_type b))) + (He':MapCast e input_bounds = Some (existT _ b e')), + Wf e'. + Proof. exact (@Wf_MapCast (Arrow s d) e Hwf input_bounds). Qed. End language. -Hint Resolve Wf_MapCast : wf. +Hint Resolve Wf_MapCast Wf_MapCast_arrow : wf. |