Matthew Daggitt

Removal of Data.Nat.Properties.Simple in v1.0 of the standard library

1

Hi, this is a ping that the module `Data.Nat.Properties.Simple` will be removed in the upcoming release of v1.0 the standard library. The module has been deprecated since v0.14. If you...

The removal of Data.Nat.Properties.Simple in v1.0 of the standard library

1

Hi, this is a ping that the module `Data.Nat.Properties.Simple` will be removed in the upcoming release of v1.0 the standard library. The module has been deprecated since v0.14. If you...

Keywords `token` and `layout` are apparently not compatible

8

When using the parser generated by the grammar fragment ``` position token TokLet {"let"}; position token TokIn {"in"}; ELet. Expr ::= TokLet "{" [Expr] "}" TokIn Expr; layout "let"; layout...

The `nonempty` macro should result in the Haskell backend using the `NonEmpty` type?

2

You can write `separator nonempty Stmt ","` in the grammar but the generated `Abs` file still uses the type `[Stmt]` rather than `NonEmpty Stmt`. This means that you have to...

Agda should report errors on `stderr` rather than `stdout`

3

It appears that Agda (v2.6.2.2) reports error messages on `stdout` rather than `stderr`. For example when you try to run `agda` on a module with the wrong module name, I...

Assume injectivity of functions during irrelevant instance search

6

Been doing a deep dive into the world of instance arguments lately in the attempt to work out how to use them better in the standard library. Came across the...

Tactic.RingSolver doesn't work over generic rings

22

Currently the reflective interface for `Tactic.RingSolver` only works over concrete instances of rings (see https://github.com/oisdk/agda-ring-solver/issues/12). It would be useful to get this working for generic rings as well.

Split `Equality` and `Order` out of `Relation.Binary`

22

Okay, the AIM discussion on Monday and reviewing https://github.com/agda/agda-stdlib/pull/1760 has crystallised something in my mind. `Relation.Binary` is fundamentally different from `Relation.Unary` and `Relation.Nullary` as it contains hierarchies for both equalities...

Deprecate `_≺_` in `Data.Fin.Base`

7

I think we already have more than enough definitions of this relation (I think this is the 5th?), and I'd prefer to have less. This is a moderately odd definition...

Remove remaining `map-with-∈` names in favour of the new `mapWith∈`

4

While going through https://github.com/agda/agda-stdlib/pull/1569 I noticed that some of the proofs for `mapWith∈` are still using the old name `map-with-∈` https://github.com/agda/agda-stdlib/blob/faa5a3cb7fde2f14cdfbd3b75ab8d08bbdc5e047/src/Data/List/Relation/Unary/Any/Properties.agda#L587 To be honest I think `mapWith∈` is a pretty...