BetterQuot

TODO:

• Developing indexed quotients (to support reasoning over cache equivalence)
• Developing more automation for lifting quotients
• ...

Build

lake +leanprover/lean4:v4.32.0 --keep-toolchain update batteries
lake build

Using BetterQuot

To import this library into your project, add the following to your lakefile.toml:

[[require]]
name = "better-quot"
git = "https://github.com/incremental-computing/better-quot"
rev = "main"

Or add the following to your lakefile.lean:

require better-quot from git "https://github.com/incremental-computing/better-quot" @ "main"

Licensing

This repository contains code under two licenses.

• Quot/ contains a small subset of files copied or adapted from the Mathlib project. These files are licensed under the Apache License 2.0. See Quot/README.md and Quot/LICENSE for details.

• All other files in this repository are original work and are licensed under the MIT License. See the repository root LICENSE.