Skip to content

Latest commit

 

History

History
25 lines (15 loc) · 1.65 KB

README.md

File metadata and controls

25 lines (15 loc) · 1.65 KB
Raw

Build Status

Data Types as Quotients of Polynomial Functors

This repository contains a formalization of data type constructions in Lean, by Jeremy Avigad, Mario Carneiro, and Simon Hudon. A preliminary version of the work is described in this talk: http://www.andrew.cmu.edu/user/avigad/Talks/qpf.pdf.

See src/README.md for a description of the contents.

The easiest way to test the code is as follows:

  • Install a precompiled binary of Lean.

  • In the root folder of this repository, type

          path-to-lean/bin/leanpkg build

    where path-to-lean is the path to the folder you just installed.

This will install a local copy of the mathlib and compile and check the dependencies as well. Lean will report any errors or sorrys. (There shouldn't be any.)

If you want to browse the files with interactive feedback from Lean, we recommend using Visual Studio Code and installing the Lean extension via the extension manager.

There are variations. For instructions that install elan, a system which will manage versions of Lean for you automatically, see here. You can also install mathlib via binaries, following the directions in the README file here.

To test the data type compiler, see test/README.md.