Commit 5c40c02d authored by Lennard Gäher's avatar Lennard Gäher
Browse files

fix

parent 3895a2ef
......@@ -66,4 +66,4 @@ theories/systemf/existential_invariants.v
#theories/stlc/cbn_logrel.v
#theories/systemf/exercices04.v
#theories/systemf/exercises04_sol.v
theories/systemf/exercises05.v
#theories/systemf/exercises05.v
......@@ -78,7 +78,7 @@ Section existential.
End existential.
Section ex4.
Import semantics.systemf_sol.logrel semantics.systemf_sol.existential_invariants.
Import logrel existential_invariants.
(** ** Exercise 4: Evenness *)
(* Consider the following existential type: *)
Definition even_type : type :=
......@@ -118,7 +118,7 @@ End ex4.
(** ** Exercise 5: Abstract sums *)
Section ex5.
Import semantics.systemf_sol.logrel semantics.systemf_sol.existential_invariants.
Import logrel existential_invariants.
Definition sum_ex_type (A B : type) : type :=
∃: ((A.[ren (+1)] #0) ×
(B.[ren (+1)] #0) ×
......@@ -140,14 +140,14 @@ End ex5.
(** ** Exercise 8: Contextual equivalence *)
Section ex8.
Import semantics.systemf_sol.binary_logrel.
Import binary_logrel.
Definition sum_ex_impl' : val :=
pack ((λ: "x", InjL "x"),
(λ: "x", InjR "x"),
(Λ, λ: "x" "f1" "f2", Case "x" "f1" "f2")
(Λ, λ: "x" "f1" "f2", Case "x" "f1" "f2")
).
Lemma sum_ex_impl'_typed n Γ A B :
Lemma sum_ex_impl'_typed n Γ A B :
type_wf n A
type_wf n B
TY n; Γ sum_ex_impl' : sum_ex_type A B.
......
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