Andreas Abel

Using `optparse-applicative` is somehow on our mental todo list, however no one has tried it out since it would be a larger refactoring (with the many options Agda has accumulated...

@szumixie @lawcho Any ideas how to fix this?

ping @valpackett > * [x] https://codeberg.org/valpackett/http-link-header/issues/1

@nad implemented option `--no-syntactic-equality` (see https://agda.readthedocs.io/en/v2.7.0.1/tools/command-line-options.html#cmdoption-no-syntactic-equality) to turn off a short-cut in equality checking. Using this should make performance _worse_, but more robust w.r.t. tiny changes (that could otherwise make...

For records, eta can be proven by matching on the record, e.g.: ```agda eta : (x : Sigma A B) -> x == (x .fst , x .snd) eta (a...

> Hi Andreas, Which definitions of `Sigma` and `==` are you using? I couldn't find them in the `Repro` module. This is just for `Agda.Builtin.{Sigma,Equality}`, but I am using ASCII...

@Soares wrote: > some variant of `no-eta-equality` that leaves behind a propositional (non-computing, postulate-like) version of the eta rule, Well, you can `postulate` eta-equality (like folks postulate functional extensionality).

Nice, thanks! If you rebase on `master`, CI should succeed. Can you please a test or an example use of the new API features? (See the `samples/` and `spec/` subdirectories...

Seems reasonable to throw this warning at use site of coinductive records rather than at definition site. We could also do the termination analysis in a way that we always...

CI run on my fork: https://github.com/andreasabel/HUnit/pull/1 `macos-latest` fails due to: - https://github.com/hspec/setup-haskell/issues/44