Skip to content

Commit

Permalink
chore: update release notes for issue #1090
Browse files Browse the repository at this point in the history
closes #1090
  • Loading branch information
leodemoura committed Apr 1, 2022
1 parent 0241d7c commit d473cc5
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion RELEASES.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,20 @@
Unreleased
---------

* [Fix inconsistency between `syntax` and kind names](https://github.com/leanprover/lean4/issues/1090).
The node kinds `numLit`, `charLit`, `nameLit`, `strLit`, and `scientificLit` are now called
`num`, `char`, `name`, `str`, and `scientific` respectively. Example: we now write
```lean
macro_rules | `($n:num) => `("hello")
```
instead of
```lean
macro_rules | `($n:numLit) => `("hello")
```

* (Experimental) New `checkpoint <tactic-seq>` tactic for big interactive proofs.

* Renamed tactic `nativeDecide` => `native_decide`.
* Rename tactic `nativeDecide` => `native_decide`.

* "Cleanup" local context before elaborating a `match` alternative right-hand-side. Examples:
```lean
Expand Down

0 comments on commit d473cc5

Please sign in to comment.