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

rm exercises

parent 16b71648
......@@ -115,43 +115,3 @@ Proof.
(*FIXME *)
Admitted.
(*Qed.*)
(** Exercise 3: Diverging term *)
Definition diverge : val :=
#0. (* FIXME *)
Lemma diverge_typed Σ n Γ :
TY Σ; n; Γ diverge : (Int Int).
Proof.
repeat solve_typing_fast.
(* FIXME *)
Admitted.
(*Qed.*)
(** Exercise 4: Fibonacci *)
Definition fibonacci : val :=
#0 (* FIXME *)
.
Lemma fibonacci_typed Σ n Γ :
TY Σ; n; Γ fibonacci : (Int Int).
Proof.
repeat solve_typing_fast.
(*FIXME *)
Admitted.
(*Qed.*)
(** Exercise 5: Counter with Reset *)
Definition make_counter : val :=
#0 (* FIXME *)
.
Lemma make_counter_typed Σ n Γ :
TY Σ; n; Γ make_counter : (Unit (Unit Int) × (Unit Unit)).
Proof.
repeat solve_typing_fast.
(* FIXME *)
Admitted.
(*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