Migrate tests from hand-rolled IO to LSpec framework

Summary

The current test suite uses hand-rolled IO Unit functions with manual IO.println "✓" / throw "✗" for pass/fail reporting. This reimplements scaffolding that existing Lean 4 testing frameworks already provide.

Current state

• 67 tests across ParserTest.lean, NfaTest.lean, MatcherTest.lean
• Each test is a def testFoo : IO Unit that manually prints results
• test/Main.lean calls each test function sequentially
• No structured output, no test counts, no failure summaries

Recommended approach: LSpec

LSpec is the standard Lean 4 testing framework. Tests become declarative assertions:

import LSpec
import Lck.Regex.Parser

def parserSuite := [
    test "single char" (parse "a" = Except.ok (Regex.char 'a')),
    test "reversed range fails" (parse "[z-a]" matches Except.error _),
    test "empty pattern" (parse "" = Except.error RegexError.emptyPattern)
  ]

def main := lspecIO $ .ofList [
    ("parser", parserSuite),
    ("matcher", matcherSuite)
  ]

Benefits:

• Eliminates ~200 lines of boilerplate (manual IO.println/throw per test)
• Structured pass/fail output with counts and summaries
• Standard lake test integration via testDriver
• Consistent with Lean ecosystem conventions

Other approaches worth considering

• #guard: Built-in compile-time assertions (#guard parse "a" = Except.ok (Regex.char 'a')). Zero boilerplate, failures are compilation errors. Good for simple invariants alongside LSpec.
• SlimCheck/Plausible: Property-based testing for discovering edge cases automatically. Could complement LSpec for properties like "any regex that parses successfully can be compiled to an NFA".

Migration plan

1. Add LSpec dependency to lakefile.toml
2. Convert each testFoo : IO Unit to an LSpec test "name" (assertion)
3. Group tests into suites by module
4. Wire up main := lspecIO $ .ofList [...]
5. Configure testDriver in lakefile
6. Remove manual IO scaffolding

Beginne mit dem Lesen von test/ParserTest.lean, test/NfaTest.lean, test/MatcherTest.lean und test/Main.lean, um die 67 bestehenden Tests und ihre aktuellen Einstiegspunkte zu verstehen. Überprüfe anschließend lakefile.toml und die Integrationsanforderungen von LSpec. Die Aufgabe ist abgeschlossen, wenn die Tests gruppierte LSpec-Suites verwenden, lake test strukturierte Ergebnisse liefert und das manuelle IO-Scaffolding entfernt wurde.