Commit d1a95033 authored by charguer's avatar charguer
Browse files

todolist

parent 0827c780
- xif sans argument pour pouvoir le forcer
- xlet_keep
let H := cfml_get_precondition tt in
xlet (... \*+ H)
- "xapp as x" pratique sur xlet
- "xapps as x" pratique sur xlet
- xlet Q => xif Q mais avec branche
MAJOR TODAY
......
......@@ -1214,6 +1214,26 @@ Qed.
Definition Sitems A (L:list A) r :=
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
(*
Section ProjLemma.
Variables (B:Type) (A1 : Type).
Variables (A2 : forall (x1 : A1), Type).
Variables (A3 : forall (x1 : A1) (x2 : A2 x1), Type).
Lemma proj_lemma_2 : forall (R:forall (x1:A1) (x2:A2 x1) (t:B), hprop),
(forall x1 x2 t, R x1 x2 t = t ~> R x1 x2).
Proof using. auto. Qed.
End ProjLemma.
Lemma Sitems_open_gen : True.
Proof.
pose (@proj_lemma_2 Sitems).
Qed.
*)
Lemma sitems_push_spec : forall (A:Type) (r:loc) (L:list A) (x:A),
app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
Proof using.
......@@ -1249,7 +1269,7 @@ xchange (Sitems_open r).
Hint Extern 1 (RegisterOpen (Sitems _)) =>
Provide Sitems_open.
Hint Extern 1 (RegisterClose (record_repr `{ nb' := _; items' := _ }')) =>
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Sitems_close.
Lemma sitems_push_spec' : forall (A:Type) (r:loc) (L:list A) (x:A),
......
......@@ -272,6 +272,10 @@ Notation "'Ret' v" :=
(!Ret (fun H Q => H ==> Q v))
(at level 69) : charac.
Notation "'Ret'' P" :=
(!Ret (fun H Q => H ==> Q (isTrue P)))
(at level 69) : charac.
Open Scope charac.
......
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