argumentcomputer / Megaparsec.lean

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

Usability: Use a more cultured non-empty list #14

Closed cognivore closed 2 years ago

cognivore commented 2 years ago

Why?

We use NonEmptyList, which is non-empty by construction. @arthurpaulino wrote something similar, except that instead of nil, he named it uno because it's never really empty. (Which is good. Nil is confusing).

Here's some functions for what @arthurpaulino called NEList: https://github.com/arthurpaulino/FxyLang/blob/master/FxyLang/Implementation/NEList.lean

And here's some proofs of correctness for them: https://github.com/arthurpaulino/FxyLang/blob/master/FxyLang/Reasoning/NEList.lean

Arthur blesses Megaparsec to copy/paste anything we need here :+1:

https://yatima.zulipchat.com/#narrow/stream/327321-yatima-tools/topic/.5BMegaparsec.2Elean.5D.20non.20empty.20lists/near/286096699

How?

cognivore commented 2 years ago

Another issue.