iris-lean
iris-lean copied to clipboard
leanprover-community
Lean 4 port of Iris, a higher-order concurrent separation logic framework
The tactic implementations need to destruct expressions (`Expr`), which is currently done by hand, i.e. using methods like `isAppOf` and `getAppArgs` in `Iris/Std/Expr.lean`. Using expression quotations would presumably simplify this...
Currently, the bidirectional entailment `⊣⊢` is defined as equality in order to use Lean's `rw` tactic to rewrite with bidirectional entailments in proofs inside the framework (e.g. in proofs of...
Currently, the proof that the length of the hypothesis mask is equal to the length of the spatial context in the implementation of `isplit` ([Tactics.lean](https://github.com/larsk21/iris-lean/blob/master/src/Iris/Proofmode/Tactics.lean)) is required to be assigned...
This MR updates the code to lean v4.10.0. This includes changing Std to Batteries and adapting the proofs. This is the first time I am working with Lean, so I...
Metadata
Owner
Metadata
Lean 4 port of Iris, a higher-order concurrent separation logic framework