G. Allais
G. Allais
I get a different error @CodingCellist ``` - + Errors (1) `-- Issue3364.idr line 6 col 0: While processing left hand side of decFn. When unifying: fromChar ' ' and:...
@dunhamsteve Is this fixed now?
Probably because I was thinking along the same lines as you: > The problem is that if you hard code the equality (e.g. by using the corresponding property from `Data.Nat.Properties`)...
#2411 addresses 1. alphabetical order of definitions (now changed to `FC`'s `startPos` order) 2. content of namespace rather than source file
The next 'obvious' extension is to be allowed to match on things usual definitions can't match on. E.g. `{-# DISPLAY Σ Nat (λ n → B) = ∃ₙ B #-}`
The danger of having issue first, implementation second is that it demands that reviewers invest a lot of time giving feedback on pie-in-the-sky proposals that never actually get implemented.
> I wonder why Agda started thinking it needs to rebuild the files? If things are imported with new (& incompatible) options then it triggers a re-checking.
I've commented on the original PR what I think may be the source of exponential blowup.
Feels like we need to stage the interface method type at declaration time so that all the `%search` are turned into concrete types.
The original bug was fixed but Steve's further examples are still failing