diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-20 23:17:22 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-20 23:17:22 -0500 |
| commit | e3497401a9df82c52d0752740a509142b2ec9220 (patch) | |
| tree | 62436dd58a34691c5ad5085d23e30bc6d9381e2a /src | |
| parent | bd88375964fc437cf14b95e2c804851175d49e6d (diff) | |
Add Wf_reify
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 0909c4284..d245e1e55 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -1012,6 +1012,9 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ Lemma Wf_Reify_as {t} v : expr.Wf (@GallinaReify.base.Reify_as t v). Proof. repeat intro; apply wf_reify. Qed. + Lemma Wf_reify {t} v : expr.Wf (fun var => @GallinaReify.base.reify var t v). + Proof. repeat intro; apply wf_reify. Qed. + Section interp. Import defaults. Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}. @@ -1061,7 +1064,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ End expr. Hint Constructors expr.wf : wf. - Hint Resolve @expr.Wf_APP expr.Wf_Reify : wf. + Hint Resolve @expr.Wf_APP expr.Wf_Reify expr.Wf_reify : wf. Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list @expr.Interp_reify @expr.Interp_APP : interp. Notation Wf := expr.Wf. |