From e04a4621687b2d22d6ea7211b3679f1f6a1cbce8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Mar 2017 19:41:10 -0400 Subject: Add Wf_MapCast_arrow --- src/Reflection/MapCastByDeBruijnWf.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src/Reflection') 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. -- cgit v1.2.3