Lars König

Go-to-definition for types in hover

4

@Kha suggested exploring how *go to definition* could look like for a type shown in a hover. It seems the front end part of this feature would work quite well,...

[RFC] Pretty Printer / Code Formatting

8

I'm currently looking into improving the pretty printer and would like to hear what you think about how we should format Lean code. This is important for many potential editor...

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...