Andreas Abel

Er, ... Ana asked me during the meeting whether there would be beginner's issues as usually repos have such and advertise them as "good first issue" or such. I am...

I am worried on how this will affect the VSCode agda-mode, I think they have a script to generate their bindings from `agda-input.el`; so I want the opinion of @banacorn...

Ping @banacorn.

During some archeology on scope checking record definition I stumbled on the commit where the open-public evil entered the garden of Eden: df2dbefe8c42186996ca642a51043530d22f6de5 🐍 🍎 > improved implementation of open...

This should be relevant: https://github.com/agda/agda/blob/f4e6fd23adb0fc551570cdd519c7c8bf61d68e03/src/full/Agda/Interaction/Imports.hs#L984-L1003 There is an option that controls the verbosity of import tracing: ``` agda --help | grep trace --trace-imports[=IMPORT_TRACING_LEVEL] print information about accessed modules during type-checking...

My question is whether it is within the policy to add a new lemma ```agda Bool-contradiction : ∀ {ℓ} {A : Set ℓ} {b : Bool} → b ≡ true...

Here is the error with a more canonical top-level module name: ``` error: [RewriteNonConfluent] Local confluence check failed: (Issue8273.ℕ.su n Issue8273.+ m) Issue8273.+ l reduces to both Issue8273.ℕ.su n Issue8273.+...

Background: > Encountered missing or private dependencies: > filepath >=1.4.100.0 &&

Documentation currently rendered at: https://agda--8235.org.readthedocs.build/en/8235/language/quote-metas.html

@rw111: For your example to work, don't you need cumulative (co)inductive types as they have in Coq: https://drops.dagstuhl.de/opus/volltexte/2018/9199/pdf/LIPIcs-FSCD-2018-29.pdf Agda does not have these yet, AFAIK.