Commit dd01b3af authored by Ralf Jung's avatar Ralf Jung

add some TODO so some stuff does not get forgotten

parent 3f715e68
Pipeline #315 passed with stage
...@@ -127,6 +127,7 @@ Lemma to_validity_op (x y : A) : ...@@ -127,6 +127,7 @@ Lemma to_validity_op (x y : A) :
to_validity (x y) to_validity x to_validity y. to_validity (x y) to_validity x to_validity y.
Proof. split; naive_solver auto using dra_op_valid. Qed. Proof. split; naive_solver auto using dra_op_valid. Qed.
(* TODO: This has to be proven again. *)
(* (*
Lemma to_validity_included x y: Lemma to_validity_included x y:
(✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y). (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
......
...@@ -385,6 +385,7 @@ Qed. ...@@ -385,6 +385,7 @@ Qed.
(* This is surprisingly different from to_validity_included. I am not sure (* This is surprisingly different from to_validity_included. I am not sure
whether this is because to_validity_included is non-canonical, or this whether this is because to_validity_included is non-canonical, or this
one here is non-canonical - but I suspect both. *) one here is non-canonical - but I suspect both. *)
(* TODO: These have to be proven again. *)
(* (*
Lemma sts_frag_included S1 S2 T1 T2 : Lemma sts_frag_included S1 S2 T1 T2 :
closed S2 T2 → S2 ≢ ∅ → closed S2 T2 → S2 ≢ ∅ →
......
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