@@ -36,6 +36,10 @@ New in 0.9.18:
36 "n". If "n" is lexically bound, then the resulting quotation will be for it,
36 "n". If "n" is lexically bound, then the resulting quotation will be for it,
37 whereas if it is not, then it will succeed with a quotation of the unique
37 whereas if it is not, then it will succeed with a quotation of the unique
38 global name that matches.
38 global name that matches.
39+* New syntax for records that closely matches our other record-like structures:
40+ type classes. See the updated tutorial for details.
41+* Records can be coinductive. Define coinductive records with the "corecord"
39* if ... then ... else ... is now built-in syntax instead of being defined in
43* if ... then ... else ... is now built-in syntax instead of being defined in
40 a library. It is shown in REPL output and error messages, rather than its
44 a library. It is shown in REPL output and error messages, rather than its
41 desugaring.
45 desugaring.
@@ -77,8 +81,6 @@ New in 0.9.17:
77* New REPL command ":core TM" that shows the elaborated form of TM along with
81* New REPL command ":core TM" that shows the elaborated form of TM along with
78 its elaborated type using the syntax of TT. IDE mode has a corresponding
82 its elaborated type using the syntax of TT. IDE mode has a corresponding
79 command :elaborate-term for serialized terms.
83 command :elaborate-term for serialized terms.
80−* Records have a new syntax based on fields rather than constructors.
81−* Records can now be coinductive.
82* Effectful and IO function names for sending data to STDOUT have been
84* Effectful and IO function names for sending data to STDOUT have been
83 aligned, semantically.
85 aligned, semantically.
84 + `print` is now for putting showable things to STDOUT.
86 + `print` is now for putting showable things to STDOUT.