G. Allais

[ admin ] first steps towards leaving CHANGELOG hell (re #521)

10

I currently only support some basic functionalities. If we are happy with the design I'll add all of the categories we are currently using. I am open to renaming the...

Refactoring `StrictToNonStrict` and `Closure.Reflexive`?

11

At the moment we have: ```agda _≤_ : Rel A _ x ≤ y = (x < y) ⊎ (x ≈ y) ``` and ```agda data ReflClosure {A : Set...

`Function`'s `case_return_of_` clashes with `RawMonad`'s `return`

5

It is very unfortunate that as soon as you write `open RawMonad m` to be able to write some monadic code, you get a parse error on `case_return_of_`. I suggest...

Started as a "quick Saturday morning project" and still not finished tonight. Currently broken but we're getting there.

Idris2 is anticlassical

1

I expect this is known but just for the sake of it, I thought I'd port [Chung Kil Hur](https://sympa.inria.fr/sympa/arc/coq-club/2010-01/msg00007.html)'s classic proof. ```idris module InjectiveTypeConstructors 0 ExcludedMiddle : Type ExcludedMiddle =...

TODO: * [ ] Correctness proofs (completeness + uniqueness) [I'm not planning to do this myself] * [ ] Examples * [ ] Use this for performance testing

We are failing to highlight some forced patterns on the LHS of a with clause. Cf. `test` (broken) vs. `test'` (working). ```idris data View : Nat -> Type where S...

* Do not steal the focus when opening the info buffer * Display the notes buffer if there are compiler warnings