Follow

I just verified that an S-expression parser recognizes only S-expressions.

Implementation: 250 LOC
Spec: 125 LOC
Proof: 700 LOC

github.com/lysxia/coq-ceres

Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!