argumentcomputer / Megaparsec.lean

Lean 4 port of Megaparsec

MIT License

22 stars 4 forks source link

Improvement: lift universes in String and Char modules or make \a \b universes independent from \w universe #25

Open cognivore opened 2 years ago

cognivore commented 2 years ago

Why?

MonadParsec is universe-polymorphic, concrete specifications like Char and String aren't.

It's ok, but our source has the same universe as our composite and atomic types, so concretisation of those causes the source go down to first universe.

How?

[ ] Make \w universe independent from \a \b
[ ] Refactor to type check and run main