A todo list for the refman

docs/refman.md

@@ -60,3 +60,10 @@ Weakest precondition calculus tactics
 
 - `wp_bind e'`: if the goal is `WP e @ E {{ Ψ }}` and `e` can be
   decomposed as `K[e']`, then turn the goal into `WP e' @ E {{ v, WP K[v] @ E {{ Q }} }}`
+
+Tactics for internal use
+------------------------
+
+- `reshape_expr e tac`: tries to non-deterministically decompose `e` as `K[e']` and calls `tac K e'`
+
+TODO: `inv_head_step`, `rewrite_closed`, `solve_closed`, `rel_bind_l/r`, `reflection.of_expr`, `value_case`