v4.23.0-rc2+patch1
Pre-release
Pre-release
- Updates the Lean 4 version
- Fixes the vararg notation (#52)
Breaking changes
- Some parts of the declaration grammar that accepted arbitrary Lean terms before have been restricted. Notably, multi-line flag and argument descriptions can now not contain inline-uses of
++anymore. It is advised to use string gaps instead.