Commit 1113f98e authored by Ralf Jung's avatar Ralf Jung

coq formatting

parent 091265d4
......@@ -7,11 +7,11 @@ Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
(* This interface keeps some of the details of the solution opaque *)
Module Type WORLD_PROP (Res : PCM_T).
(* PreProp: The solution to the recursive equation. Equipped with a discrete order *)
(* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
Parameter PreProp : cmtyp.
Instance PProp_preo: preoType PreProp := disc_preo PreProp.
Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp.
Instance PProp_ext : extensible PreProp := disc_ext PreProp.
Instance PProp_preo : preoType PreProp := disc_preo PreProp.
Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp.
Instance PProp_ext : extensible PreProp := disc_ext PreProp.
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
......@@ -24,7 +24,6 @@ Module Type WORLD_PROP (Res : PCM_T).
Instance Props_preo : preoType Props| 1 := _.
Instance Props_pcm : pcmType Props | 1 := _.
(* Establish the recursion isomorphism *)
Parameter ı : PreProp -n> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -n> PreProp.
......@@ -32,6 +31,7 @@ Module Type WORLD_PROP (Res : PCM_T).
Axiom isoR: forall T, ı (ı' T) == T.
End WORLD_PROP.
(* Now we come to the actual implementation *)
Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
......
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