Commit 54067433 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add typing for value poly-lambdas.

parent 9a99553c
......@@ -241,4 +241,11 @@ Section compatibility.
iApply (env_sem_typed_insert with "IH").
iApply (env_sem_typed_insert with "[$]"). iApply env_sem_typed_empty.
Qed.
Lemma TLamV_sem_typed e C : ( A, e : C A) - (Λ: e) : A, C A.
Proof.
iIntros "#H !#" (A) "/=". wp_pures.
rewrite -{2}(subst_map_empty e). iApply ("H" $! A).
by iApply env_sem_typed_empty.
Qed.
End compatibility.
......@@ -92,5 +92,7 @@ Section fundamental.
change ( ?τ1 _ ?τ2 _)%sem_ty with ( τ1 τ2 ρ).
rewrite -(interp_env_empty ρ) -!interp_env_binder_insert.
by iApply fundamental.
+ iApply TLamV_sem_typed; iIntros (A).
rewrite -(interp_env_empty (A :: ρ)). by iApply fundamental.
Qed.
End fundamental.
......@@ -135,6 +135,9 @@ with val_typed : val → ty → Prop :=
| RecV_typed f x e τ1 τ2 :
binder_insert f (TArr τ1 τ2) (binder_insert x τ1 ) e : τ2
RecV f x e : TArr τ1 τ2
| TLamV_typed e τ :
e : τ
(Λ: e) : TForall τ
where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ v : τ" := (val_typed v τ).
......
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