sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

doc: fix broken code blocks in RELEASES.md (#6527)

Browse Source 
just fix markdown
This commit is contained in:
Kitamado
2025-01-04 17:08:12 +09:00
committed by GitHub
parent 639e6e92a4
commit 31435e9cd1
1 changed files with 2 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
RELEASES.md
View File

@@ -107,6 +107,7 @@ For `Prop`, these tactics now suggest the `by_cases` tactic. Example:
```
tactic 'cases' failed, major premise type is not an inductive type
Prop
```
* [#6381](https://github.com/leanprover/lean4/pull/6381) fixes a bug in `withTrackingZetaDelta` and
`withTrackingZetaDeltaSet`. The `MetaM` caches need to be reset. See new
@@ -783,6 +784,7 @@ full structure lvals. Examples of these for structure instance notation:
structure PosFun where
f : Nat → Nat
pos : ∀ n, 0 < f n
```
- [#6168](https://github.com/leanprover/lean4/pull/6168) extends the "motive is not type correct" error message for the
rewrite tactic to explain what it means. It also pretty prints the