Commit Graph

12 Commits

Author SHA1 Message Date
G. Allais
9e7625e613
[ log ] more readable output for elab.ambiguous (#1500) 2021-06-03 18:19:08 +01:00
Edwin Brady
7f210b52aa Inline small metavariables
Where 'small' means they don't refer to other metavariables, except
right at the top level, and they don't go beyond a certain small depth,
arrived at by experimenting.

We already did a bit of this, but only for depth 0. The effect of this
is that we don't need to save out lots of metavariables, so ttc loading
is faster. This takes about 8s off the Idris build time!
2021-05-18 17:56:36 +01:00
G. Allais
ab241213f3
[ breaking ] making toList part of Foldable (#1395) 2021-05-11 08:26:00 +01:00
Denis Buzdalov
583442b359
[ contrib ] Arithmetic on Fin (#830)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-04-23 12:05:13 +01:00
G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' (#1093) 2021-03-01 08:29:43 +00:00
Guillaume ALLAIS
7ccc47712e [ re #1087 ] Better error messages in the REPL
(as well as in type signatures now that I know how to do that)
2021-02-19 12:34:19 +00:00
Yu Zhang
08a35d694c
Improving error messages (#786)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2020-11-26 11:35:55 +00:00
Christian Rasmussen
091465525b Remove FArgList 2020-09-23 18:33:19 +01:00
G. Allais
a0c0974676
[ debug ] pretty printer for case trees (#652) 2020-09-09 16:22:22 +01:00
Guillaume ALLAIS
e64a3e910c [ test ] cleanup basic044
All of these internal names are making the output fragile. This
cleanup should allow us to only have to update the golden file
when there is a genuinely interesting change.
2020-08-25 09:33:39 +01:00
Alex Gryzlov
ef5299733a
refactor Data.String.Parser (#579) 2020-08-22 08:13:34 +01:00
G. Allais
da78ac4783
[ new ] topics for logging levels (#569) 2020-08-20 18:45:34 +01:00