@@ -2,8 +2,29 @@
3## Language updates
3## Language updates
5+* `rewrite` can now be used to rewrite equalities on functions over
5* `rewrite` can now be given an optional rewriting lemma, with the syntax
7* `rewrite` can now be given an optional rewriting lemma, with the syntax
6 `rewrite [rule] using [rewrite_lemma] in [scope]`.
8 `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:
13+ data SnocList : List a -> Type where
15+ Snoc : SnocList xs -> SnocList (xs ++ [x])
17+ snocList : (xs : List a) -> SnocList a
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
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`.
8## Miscellaneous updates
29## Miscellaneous updates