max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: formatting/capitalization in RELEASES.md

Browse source 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
This commit is contained in:
Adrien Champion 2023-03-02 10:11:07 +01:00 • committed by Sebastian Ullrich
parent 5111595753
commit ce0d2a6928
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASES.md
View file

@ -1,10 +1,10 @@
Unreleased
---------
* [make `calc` require the sequence of relation/proof-s to have the same indentation](https://github.com/leanprover/lean4/pull/1844),
and [add `calc` alternative syntax allowing underscores `_` in the first relation](https://github.com/leanprover/lean4/pull/1844)
* [Make `calc` require the sequence of relation/proof-s to have the same indentation](https://github.com/leanprover/lean4/pull/1844),
and [add `calc` alternative syntax allowing underscores `_` in the first relation](https://github.com/leanprover/lean4/pull/1844).
the flexible indentation in `calc` was often used to align relations/proofs
The flexible indentation in `calc` was often used to align the relation symbols:
```lean
example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc
@ -15,7 +15,7 @@ Unreleased
_ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc]
```
this is no longer legal, but the alternative syntax accomplishes essentially the same goal with proper indentation:
This is no longer legal. The new syntax puts the first term right after the `calc` and each step has the same indentation:
```lean
example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc (x + y) * (x + y)