@@ -2,8 +2,29 @@
22
33## Language updates
44
5+* `rewrite` can now be used to rewrite equalities on functions over
6+ dependent types
57* `rewrite` can now be given an optional rewriting lemma, with the syntax
68 `rewrite [rule] using [rewrite_lemma] in [scope]`.
9+* Experimental extended `with` syntax, which allows calling functions defined
10+ in a with block directly. For example:
11+
12+```
13+ data SnocList : List a -> Type where
14+ Empty : SnocList []
15+ Snoc : SnocList xs -> SnocList (xs ++ [x])
16+
17+ snocList : (xs : List a) -> SnocList a
18+
19+ my_reverse : List a -> List a
20+ my_reverse xs with (snocList xs)
21+ my_reverse [] | Empty = []
22+ my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p
23+```
24+
25+ The `| p` on the right hand side means that the `with` block function will
26+ be called directly, so the recursive structure of `SnocList` can direct the
27+ recursion structure of `my_reverse`.
728
829## Miscellaneous updates
930