G. Allais

Bug in the string literal parser?

1

While I was porting the JSON parser to Agda yesterday I think I have found a bug in the string literal parser: https://github.com/gallais/idris-tparsec/blob/75b288719b9781273a595c294b7d3bed5ea1904d/src/TParsec/Combinators/Chars.idr#L154-L156 After having read a `\` we will...

I am not sure how much of the time spent parsing examples is actually spent computing the whole `Parser mn p a n` for the concrete size `n` of the...

Add various `parse` functions

2

The one function in `TParsec.Running` is only ever useful to write down examples but not to actually use it. It'd be nice to have specialised runners for input `String` vs....

Seeing how #17 fixes a lot of these, it would be nice to always keep the files clean. Cf. https://github.com/agda/agda/tree/master/src/fix-agda-whitespace for how it's done in the agda repo.

Feature request: Allow compile-time substitution of definitions

2

In agda/agda-stdlib#1427 we have a conundrum: we'd like to define an efficient version of min but it would be inconvenient when used at the type level. Andreas suggests defining a...

Add support for do-notations in agda-mode's give

1

It's currently impossible to use `give` (`C-c C-space`) on the following hole: ```agda postulate M : Set → Set _>>=_ : ∀ {A B} → M A → (A →...

agda-mode: generate function template from type signature

1

```agda f : (A B : Set) -> Set -> Set -- ^ C-c C-c on `f` should generate f A B x = ? ```

A variant C-c C-d for the identifier under the cursor

1

A command that gets Agda to find and display the type of the identifier under the cursor. This should work in: * [ ] Import lists * [ ] LHS...

[ re #952, #356, #939, #1530 ] Overhaul of Functor/Applicative/Monad

2

TODO: * [ ] CHANGELOG * [x] #1530

JOSS submission?

18

TIL https://joss.theoj.org/ gives us the opportunity to "publish" the stdlib as a small journal paper. This would give people a standard way of citing the lib & crediting the contributors