From 31435e9cd156ecc53c7070b5dd061b98d95187ab Mon Sep 17 00:00:00 2001 From: Kitamado <47292598+Seasawher@users.noreply.github.com> Date: Sat, 4 Jan 2025 17:08:12 +0900 Subject: [PATCH] doc: fix broken code blocks in RELEASES.md (#6527) just fix markdown --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index a657a38bd898..d1958e403f8f 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -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