Skip to content
Snippets Groups Projects
Commit be24d0bd authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Nits

parent 2b955907
No related branches found
No related tags found
No related merge requests found
......@@ -56,7 +56,7 @@ Section compute_example.
Definition compute_type_client_aux (A : ltty Σ) (rec : lsty Σ) : lsty Σ :=
lty_select $ <[cont := (<!!> TY () A; <??> TY A ; rec)%lty]> $
<[stop := END%lty]>∅.
Instance compute_type_rec_client_contractive A :
Instance compute_type_client_contractive A :
Contractive (compute_type_client_aux A).
Proof. solve_proto_contractive. Qed.
Definition compute_type_client A : lsty Σ :=
......
......@@ -15,14 +15,14 @@ Definition compute_service : val :=
(λ: "c", let: "v" := recv "c" in
send "c" ("v" #());; "go" "c")
(λ: "c", #()).
Section compute_example.
Context `{heapG Σ, chanG Σ, spawnG Σ}.
Definition compute_type_service_aux (rec : lsty Σ) : lsty Σ :=
lty_branch $ <[cont := (<?? A> TY () A; <!!> TY A ; rec)%lty]> $
<[stop := END%lty]> $ ∅.
Instance mapper_type_rec_service_contractive :
Instance mapper_type_service_contractive :
Contractive (compute_type_service_aux).
Proof. solve_proto_contractive. Qed.
Definition compute_type_service : lsty Σ :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment