From dd15798b835d676288d741ce6cf13ab7dfc440cc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 17 Aug 2018 04:07:11 -0400 Subject: Be more judicious about an instance --- src/Experiments/NewPipeline/LanguageWf.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index be24ca48d..b5a62687c 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -97,7 +97,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed. End app_curried_instances. - Global Instance and_eqv_for_each_lhs_of_arrow_not_higher_order {base_type base_interp t} + Lemma and_eqv_for_each_lhs_of_arrow_not_higher_order {base_type base_interp t} (Ht : type.is_not_higher_order t = true) (v : @type.for_each_lhs_of_arrow base_type (type.interp base_interp) t) : Proper (type.and_for_each_lhs_of_arrow (@type.eqv) (t:=t)) v. @@ -108,6 +108,8 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ eauto. Qed. + Global Hint Immediate and_eqv_for_each_lhs_of_arrow_not_higher_order : typeclass_instances. + Lemma related_hetero_iff_app_curried {base_type base_interp1 base_interp2 R} t F G : (@type.related_hetero base_type base_interp1 base_interp2 R t F G) <-> (forall x y, type.and_for_each_lhs_of_arrow (@type.related_hetero base_type base_interp1 base_interp2 R) x y -> R (type.final_codomain t) (type.app_curried F x) (type.app_curried G y)). -- cgit v1.2.3