Commit 66f01d1c authored by Robbert Krebbers's avatar Robbert Krebbers

Make type_soundness a corollary.

parent dd8e7e9a
...@@ -13,7 +13,7 @@ Proof. ...@@ -13,7 +13,7 @@ Proof.
iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. by iApply interp_env_nil. iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. by iApply interp_env_nil.
Qed. Qed.
Lemma type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] ⊢ₜ e : τ [] ⊢ₜ e : τ
rtc step ([e], σ) (e' :: thp, σ') rtc step ([e], σ) (e' :: thp, σ')
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
......
...@@ -16,7 +16,7 @@ Proof. ...@@ -16,7 +16,7 @@ Proof.
repeat iSplit; eauto. by iApply interp_env_nil. repeat iSplit; eauto. by iApply interp_env_nil.
Qed. Qed.
Lemma type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] ⊢ₜ e : τ [] ⊢ₜ e : τ
rtc step ([e], σ) (e' :: thp, σ') rtc step ([e], σ) (e' :: thp, σ')
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
......
...@@ -16,7 +16,7 @@ Proof. ...@@ -16,7 +16,7 @@ Proof.
repeat iSplit; eauto. by iApply interp_env_nil. repeat iSplit; eauto. by iApply interp_env_nil.
Qed. Qed.
Lemma type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] ⊢ₜ e : τ [] ⊢ₜ e : τ
rtc step ([e], σ) (e' :: thp, σ') rtc step ([e], σ) (e' :: thp, σ')
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment