From 9a193f595be3b1087fb0f416e1a4a31b52619c14 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 16 Nov 2024 14:08:32 +0900 Subject: [PATCH] =?UTF-8?q?=E3=82=BF=E3=82=A4=E3=83=9D=20Fixes=20#1107?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean b/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean index 22c59df5..a8635f6d 100644 --- a/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean +++ b/LeanByExample/Reference/Declarative/DeclareSyntaxCat.lean @@ -30,11 +30,11 @@ def setOf (p : α → Prop) : Set α := p declare_syntax_cat binder /-- `{x : T | P x}` の `: T` の部分。 -あってもなくて良いので `( )?` で囲う -/ +あってもなくても良いので `( )?` で囲う -/ syntax ident (" : " term)? : binder /-- `{x ∈ T | P x}` の `∈ T` の部分。 -あってもなくて良いので `( )?` で囲う -/ +あってもなくても良いので `( )?` で囲う -/ syntax ident (" ∈ " term)? : binder /-- 集合の内包表記 -/