affine-constructive-maths

A library of constructive mathematics using affine logic, following Michael Shulman's "Affine logic for constructive mathematics."¹, and heavily inspired by the MathClasses library.

Building

Compiles with Coq 8.17.0. To build:

git clone https://github.com/jlottes/affine-constructive-maths.git
cd affine-constructive-maths
coq_makefile -f _CoqProject -o Makefile
make

Footnotes

1. Shulman, Michael. "Affine logic for constructive mathematics." Bulletin of Symbolic Logic 28.3 (2022): 327-386. ↩