From 002412e9d0465abf6cb17d0995fbef3f45f260e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Mar 2022 17:08:54 -0800 Subject: [PATCH] chore: missing code block annotation --- RELEASES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index a0ea3c48b2..0999ebe004 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -155,7 +155,7 @@ inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where ``` * Eliminate auxiliary type annotations (e.g, `autoParam` and `optParam`) from recursor minor premises and projection declarations. Consider the following example -``` +```lean structure A := x : Nat h : x = 1 := by trivial