parse_failure command

Stream: Is there code for X?

[Asei Inoue]

here is my command which run parser

infix:60 " ⋄ " => Nat.mul

open Lean Parser in

def parse (cat : Name) (s : String) : MetaM Syntax := do
  ofExcept <| runParserCategory (← getEnv) cat s

#eval parse `term "1 ⋄ 2 ⋄ 3"

but I want to create #parse_failure command which succeed only when parse fails.

[Robin Arnez]

If you want this for testing, #guard_msgs might suffice:

import Lean

infix:60 " ⋄ " => Nat.mul

open Lean Parser in

def parse (cat : Name) (s : String) : MetaM Syntax := do
  ofExcept <| runParserCategory (← getEnv) cat s

/-- error: <input>:1:6: expected end of input -/
#guard_msgs in
#eval parse `term "1 ⋄ 2 ⋄ 3"

[Asei Inoue]

I know guard_msgs

[Asei Inoue]

I want to display my intension by command name, and to display in better form…

[Aaron Liu]

Using #guard_msgs is usually preferable to commands like #check_failure because you can guard the error message too.

[Aaron Liu]

Asei Inoue said:

I want to display my intension by command name, and to display in better form…

You can use a macro that expands into #guard_msgs.

[Damiano Testa]

By the way, mathlib has a #parse command in Mathlib.Util.ParseCommand that seems quite similar to your parse function.