G. Allais

[ compat ] with current Idris

6

Following https://github.com/idris-lang/Idris2/issues/1291 here is an updated version of the code in this repository to work with the current dev version of idris. Unfortunately I don't know how to install multiple...

[ fix #326 ] Interleaving let binding and declarations

2

This is a work in progress. Compilation currently fails with the following internal error: idris: Erasure.hs:lamToLet': unexpected input: vs = [{eta_4}], tm = Idris.Parser.case block in case block in mkLets...

Very easy to reproduce this internal error: ```shell touch Test idris2 Test ``` gives us: > Uncaught error: INTERNAL ERROR: build/ttc/Test.ttc: File Not Found

`with` on steroids

4

Listing things I do not want to forget before AIM XXX. * [x] Internalising inspect (#4084) * [x] Implicit with (#4078) * [x] Irrelevant with (more generally: control over modalities)...

Case-split on a datatype defined in a parametrised module produces needlessly-prefixed patterns

12

When case-splitting on `x` in `B.agda`, we get the pattern `(;A.A⁺.a x)` which is a parse error rather the completely valid `(a x)`. `A.agda`: ```agda open import Level module A...

A more declarative auto-cong machinery

2

I have written a little bit of declarative congruence magic: https://github.com/gallais/potpourri/blob/b0b734fb8e768f280bc36519048b977b994d1a5e/agda/cong/Syntax/Focus.agda Unlike the content of [`Tactic.Cong`](http://agda.github.io/agda-stdlib/Tactic.Cong.html), it is not trying to guess what the context should be but instead reads...

Fix the mentions of defunct `README` modules

6

In [Data.Nat.Tactic.RingSolver](http://agda.github.io/agda-stdlib/Data.Nat.Tactic.RingSolver.html) we tell people to > See README.Nat for examples of how to use this solver But `README.Nat` does not exist anymore. We probably meant to point to [README.Tactic.RingSolver](http://agda.github.io/agda-stdlib/README.Tactic.RingSolver.html)...

Cf. the code in https://github.com/agda/agda/tree/master/notes/reflection developed during the Edinburgh AIM.

Data.List.Membership.Setoid should re-export Any's constructors

5

It's pretty annoying to have to import 2 modules every time we want to do anything with membership proofs.

Definition with no RHS is incorrectly accepted as total

13

Found while looking at the code interactively generated by case splitting in #2242. ```idris %default total g : Not Bool g () impossible f : Void f = g True...