Skip to content

avigad/qpf

master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.

About

Datatypes as quotients of polynomial functors

Resources

License

Stars

Watchers

Forks

Packages

No packages published