Commit 6a0ef8e0 authored by Robbert Krebbers's avatar Robbert Krebbers

More typing examples.

parent 27818ed2
......@@ -189,14 +189,9 @@ Proof.
- apply Val_typed, UnitV_typed.
Qed.
Definition swap : val := λ: "l1" "l2",
let: "x" := !"l1" in
"l1" <- !"l2";;
"l2" <- "x".
Lemma swap_typed τ : swap : (ref τ ref τ ()).
Proof.
unfold swap.
rewrite /swap.
apply LamV_typed.
apply Lam_typed.
apply Let_typed with τ.
......@@ -209,3 +204,39 @@ Proof.
- by apply Var_typed.
- by apply Var_typed.
Qed.
Lemma swap_poly_typed : swap_poly : (∀: ref #0 ref #0 ()).
Proof.
rewrite /swap_poly.
apply TLamV_typed.
do 2 apply Lam_typed.
apply Let_typed with (#0)%ty.
{ apply Load_typed. by apply Var_typed. }
apply Seq_typed with ()%ty.
{ apply Store_typed with (#0)%ty.
- by apply Var_typed.
- apply Load_typed. by apply Var_typed. }
apply Store_typed with (#0)%ty.
- by apply Var_typed.
- by apply Var_typed.
Qed.
Lemma unsafe_pure_not_typed Γ τ : ¬ (Γ unsafe_pure : τ).
Proof.
intros Htyped.
repeat
match goal with
| H : _ _ : _ |- _ => inversion H; simplify_eq/=; clear H
| H : _ : _ |- _ => inversion H; simplify_eq/=; clear H
end.
Qed.
Lemma unsafe_ref_not_typed Γ τ : ¬ (Γ unsafe_ref : τ).
Proof.
intros Htyped.
repeat
match goal with
| H : _ _ : _ |- _ => inversion H; simplify_eq/=; clear H
| H : _ : _ |- _ => inversion H; simplify_eq/=; clear H
end.
Qed.
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