Caution
Work on lean-iris has restarted! To consolidate the effort, this project is no longer active. Interested contributors should work on lean-iris instead.
This project is an implementation for some of the data structures of Iris in Lean.
While the ultimate goal of the project is to support lean-iris with a fully-fledged Iris implementation, the current target is to mechanize enough of the foundations to instantiate the frontend with upred.
The main mechanized results so far:
- Semi-bundled hierarchy for (C)OFE
- Nonexpansive and contractive maps
- OFE instances:
- OFE on (bundled) nonexpansive maps
- discreteO, laterO, leibnizO, prodO
- Bundled (C)OFE:
- The category of (C)OFE and nonexpansive maps
- The category OFE is cartesian closed
- A definition for oFunctor
- The category of (C)OFE and nonexpansive maps
- Fixpoint of contractive maps
Future steps are described in Eileen: A plan for Iris in Lean.
Do not run lake update without a PR.
This project tracks the lake-manifest file in order to pin the mathlib version.
PR's regarding code improvements, CI, and compliance with the Mathlib style guide are very welcome!
If you would like to contribute to the main porting effort please get in touch with me at @markusdemedeiros on the Lean Zulip, or by email, in order to avoid redundant work.