Skip to content

Commit

Permalink
doc: fix broken code blocks in RELEASES.md (#6527)
Browse files Browse the repository at this point in the history
just fix markdown
  • Loading branch information
Seasawher authored Jan 4, 2025
1 parent 639e6e9 commit 31435e9
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 31435e9

Please sign in to comment.