argumentcomputer / Megaparsec.lean

Lean 4 port of Megaparsec
MIT License
22 stars 4 forks source link

Module structure, #13 #16

Closed DanielRrr closed 2 years ago

DanielRrr commented 2 years ago

The patch solves #13

Problem: at the moment most of the definitions are introduced in a single module. This mishmash makes the developer in this project arrangement because it has not logical structure.

Solution: we classify all definitions introduced earlier according to their semantic role. We will have Error.lean with some Error data types, RWST.lean with the RWST monad and related function, Util.lean with useful functions which are not specific for parsing logic, Stream.lean for Stream related definitions.