File size: 573 Bytes
0115dcf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 | 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))
|