Patrick Massot

The exercise about ``` def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) (a b : StandardSimplex n) : StandardSimplex n...

Code action for induction ... using ...

1

The current induction code action is really nice, but it doesn't work when using a non-default induction rule.

### Proposal It would be nice to have an action to de-select everything in the info view, hopefully with an assigned default key-binding. Currently this is not crucial. But several...

Installing issues on Ubutun 22.04

1

Thanks for providing this software.! I tried to follow the installation instructions on Ubuntu 22.04. First the opam ppa doesn't work (at least not with Ubuntu 22.04). So I went...

feat: the largest T2 quotient of a topological space.

1

--- [](https://gitpod.io/from-referrer/)

Using ``` {include VersoTest.Introduction.Getting_Started} {include VersoTest.Introduction.Overview} ``` which misses a blank line turns up the unhelpful message: ``` unexpected syntax failed to pretty print term (use 'set_option pp.rawOnError true' for...

### Proposal This is somehow a meta-RFC that aims to track some general issue that probably involves several different technical questions. It is created in the context of providing the...

feat: Unfold widget

2

--- [](https://gitpod.io/from-referrer/)

The `induction'` tactic is only a porting hack, we need to teach the Lean 4 way.

Given all the recent change on simp and zeta reduction, we need to review our explanations and make sure they are still useful.