From 407bbf3b465ea6e1291cf5b0e27e907b668fcfa7 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 17 Nov 2024 03:02:58 +0900 Subject: [PATCH] =?UTF-8?q?=E3=82=B3=E3=83=BC=E3=83=89=E3=82=92=E7=B0=A1?= =?UTF-8?q?=E7=95=A5=E5=8C=96=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Type/Syntax.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/LeanByExample/Reference/Type/Syntax.lean b/LeanByExample/Reference/Type/Syntax.lean index b43b240..d0f491b 100644 --- a/LeanByExample/Reference/Type/Syntax.lean +++ b/LeanByExample/Reference/Type/Syntax.lean @@ -57,8 +57,7 @@ open Lean Parser /-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/ def parse (cat : Name) (s : String) : MetaM Syntax := do - let .ok s := runParserCategory (← getEnv) cat s | throwError s - return s + ofExcept <| runParserCategory (← getEnv) cat s -- `true` は識別子としてパースされている。 /--