---

name: parsing description: Use the lean4-parser library for parsing structured input. Invoke when implementing parsers for AoC puzzles or other text processing tasks in Lean. allowed-tools: Read, Edit, Write

Parsing Skill: lean4-parser Library

When parsing structured input (especially for AoC puzzles), use the lean4-parser library instead of manual string splitting.

Installation

Already configured in lakefile.toml:

Copy[[require]]
name = "Parser"
git = "https://github.com/fgdorais/lean4-parser"
rev = "main"

Import

Copyimport Parser
open Parser Char

Quick Reference

Parser Types

Copy-- Use SimpleParser for good error messages
abbrev MyParser := SimpleParser Substring Char

Running Parsers

Copymatch myParser.run inputString with
| .ok _ result => -- use result
| .error _ e => -- handle error

Common Combinators

Example: Parse Numbers from Line

Copydef parseLine : SimpleParser Substring Char (List Nat) := do
  sepBy ASCII.parseNat (dropMany1 (char ' '))

Example: Parse Coordinates

Copydef parseCoord : SimpleParser Substring Char (Int × Int) := do
  let _ ← char '('
  let x ← ASCII.parseInt
  let _ ← char ','
  dropMany space
  let y ← ASCII.parseInt
  let _ ← char ')'
  return (x, y)

Example: Parse Key-Value Pairs

Copydef parseKeyValue : SimpleParser Substring Char (String × Int) := do
  let key ← takeMany1 alpha
  let _ ← char ':'
  dropMany space
  let value ← ASCII.parseInt
  return (⟨key⟩, value)

Example: Parse with Alternatives

Copydef parseDirection : SimpleParser Substring Char Int := first [
  string "up" *> pure 1,
  string "down" *> pure (-1),
  string "left" *> pure 0,
  string "right" *> pure 0
]

Example: Looping Until End

Copydef parseAll : SimpleParser Substring Char (List Int) := do
  let mut results := []
  while !(← test endOfInput) do
    let n ← ASCII.parseInt
    results := results ++ [n]
    dropMany (char ' ' <|> char '\n')
  return results

Documentation

• Full docs: https://www.dorais.org/lean4-parser/doc/
• Repository: https://github.com/fgdorais/lean4-parser