Commit d1a2a63a authored by Dan Frumin's avatar Dan Frumin

Start writing the documentation

parent eddf490d
iris-logrel reference manual
============================
Threadpool tactics
------------------
- `tp_normalise j`: simplify the term/expression in `j ⤇ e`
- `tp_bind j e'`: if `j ⤇ e` and `e` can be decomposed as `K[e']`,
then turn the resource into `j ⤇ K[e']`. For example if, `j ⤇ f (!x + 2)`,
then invoking `tp_bind j (Load x)` converts the resource
to `j ⤇ fill [AppRCtx f, PlusLCtx 2] (!x)`.
- `tp_store j`
- `tp_load j`
- `tp_rec j`
- `tp_op j`
- `tp_cas_fail j` and `tp_cas_suc j`
- `tp_fork i as j "Hj"`
+ `tp_fork i as j` is the same thing as `let H := iFresh in tp_fork i as j H`
+ `tp_fork i` has a similar behaviour, but...
- `tp_apply j lem with "H1 ... Hn" as "S"`
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