Formalization of linear logic proof-nets for multiplicative linear logic in the spirit of the Yalla library.
Requires:
- OLlibs (add-ons for the standard library): see installation instructions.
- Graph Theory (library for graphs): see installation instructions.
- Mczify (lia for MathComp): see installation instructions.
Tested with Coq 8.18.0, MathComp 2.0.0, Ollibs 2.0.5, Graph Theory 0.9.3, Mczify 1.5.0+2.0+8.16.