Andreas Abel
Andreas Abel
@copilot I assign to you the task to implement this PR according to the description I wrote in the previous comment.
In 2014 I sketched a new semantics for record declarations: W.l.o.g., a record declaration looks like this: (`d1`..`d3` are declarations, [...] says explicitly what is in scope) ``` agda record...
@Blaisorblade : Yes, that would be the goal.
The main challenge is to build the constructor type. How about this simpler semantics, if we cheat a bit: ```agda postulate R : P -> Set module R (p :...
Putting out some ideas: The point of surgery would be here: https://github.com/agda/agda/blob/7c43e5fd295c10df573927fd52eef27c7c16395d/src/full/Agda/Termination/TermCheck.hs#L871-L882 Argument normalization in recursive calls was turned off as it was too expensive. Maybe we dedicate a new...
UPDATE: Forget this comment altogether: There is something very odd here, because success also depends on the argument order: ```agda works : Nat → Nat → Nat works (suc n)...
Minimalized: ```agda open import Agda.Builtin.FromNat using (Number; fromNat) -- fromNat needs to be in scope visible open import Agda.Builtin.Nat using (Nat; zero; suc) open import Agda.Builtin.Unit using (⊤) instance NumNat...
This is not a bug, it is a deficiency of higher-order unification. If you make all argument explicit, you get the following: ```agda Pred : Set → Set₁ Pred X...
> I suppose one thing that could make it easier to deal with this is to have an `agda-mode` keybinding that automatically turns an unsolved constraint into an explicit hole,...