Jesper Cockx
Jesper Cockx
In https://github.com/agda/agda/pull/5897, @plt-amy suggested that perhaps we should hide the support for indexed inductive types with --cubical behind a flag, since the current implementation is not yet complete and will...
Consider the following example: ```agda module _ where record R (N : Set) : Set₁ where field g : N → Set open R {{...}} module _ {N : Set}...
A significant fraction of bugs in Agda (or at least, in the parts of Agda that I tend to work on) are somehow caused by messing up de Bruijn indices...
It would be good to work towards a release of 2.6.3 before the next Agda meeting, i.e. by the end of October. To get us started, I went through all...
(forked off from the discussion at https://github.com/agda/agda/issues/5731) ```agda open import Agda.Builtin.IO open import Agda.Builtin.List open import Agda.Builtin.Reflection renaming (bindTC to _>>=_) open import Agda.Builtin.String open import Agda.Builtin.Unit macro getMeta :...
Minimal example: ```agda open import Agda.Builtin.Nat open import Agda.Builtin.Sigma data D : Set where c : ((x , y) : Σ Nat λ _ → Nat) → D foo :...
See https://github.com/agda/agda/issues/1625#issuecomment-1091699806
This PR contains a few refactoring that I did while working on https://github.com/agda/agda/pull/6679 before giving up on that PR.
When playing around with instances, I noticed that Agda was reducing them even when doing so is not needed. Here is an example (with a looping function to clearly demonstrate...
Since 2013 (https://github.com/agda/agda/commit/3777ddf8967b1810cdb7d543a7652ff40d2f7365) Agda has support for let-bindings in telescopes, e.g. `(x : Nat) (let y = x + x) (v : Vec Nat y) -> ...`. However as far...