diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-08-17 04:07:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-08-17 04:07:11 -0400 |
| commit | dd15798b835d676288d741ce6cf13ab7dfc440cc (patch) | |
| tree | d9018db3f85d53320e4565167d9654d7af13cc64 /src | |
| parent | c8af4ec0e33b08a17b378ab2b47ea8c55d58b2ef (diff) | |
Be more judicious about an instance
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 4 |
1 files changed, 3 insertions, 1 deletions
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)). |