コードを簡略化する

lean-ja · Nov 16, 2024 · 407bbf3 · 407bbf3
1 parent eae5d0f
commit 407bbf3
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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` は識別子としてパースされている。
 /--