diff options
author | 2017-05-16 23:07:25 -0400 | |
---|---|---|
committer | 2017-05-16 23:07:25 -0400 | |
commit | 55b011d85e1477a5b591fa74cc65316b9a49364e (patch) | |
tree | 3ab8264137957d251a9a99cdf8eb29c52e12547f /src/Compilers/Named/WfInterp.v | |
parent | e2956617c26998eaee2d6228eac600f84136c285 (diff) |
Flip argument order on interp for easier Proper lemmas
Diffstat (limited to 'src/Compilers/Named/WfInterp.v')
-rw-r--r-- | src/Compilers/Named/WfInterp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v index 580dcb438..e9cd8737c 100644 --- a/src/Compilers/Named/WfInterp.v +++ b/src/Compilers/Named/WfInterp.v @@ -15,7 +15,7 @@ Section language. Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t} (Hwf : prop_of_option (wff ctx e)) - : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None. + : @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None. Proof using Type. revert dependent ctx; induction e; repeat first [ progress intros @@ -34,7 +34,7 @@ Section language. Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t} (Hwf : wf ctx e) v - : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None. + : @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None. Proof using Type. destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto. Qed. |