| import LSpec | |
| import Pantograph.Elab | |
| import Test.Common | |
| open Lean | |
| namespace Pantograph.Test.Parser | |
| abbrev TestM := TestT $ Elab.TermElabM | |
| def test_runParserCategory : TestM Unit := do | |
| let .ok (stx, pos) := runParserCategory' (← getEnv) `tactic "intro n\ncases n" | |
| | fail "Tactic failed to parse" | |
| checkEq "stx" (toString stx.prettyPrint) "intro n" | |
| checkEq "pos" pos.byteIdx 8 | |
| def suite (env : Environment) : List (String × IO LSpec.TestSeq) := | |
| [ | |
| ("runParserCategory", test_runParserCategory), | |
| ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) | |