Andreas Abel
Andreas Abel
@rhendric Will you continue to maintain the `record where` feature?
@rhendric : Well, it is your baby, crying for attention, are going to give it the care it needs? Agda is an open-source project maintained by volunteers. There is no...
@rhendric Thanks for clarifying your position. I apologize if your felt that your work was taken from you, this was not my intention. Git does not properly track authorship if...
This adds new features for idiom brackets, changing the course of action for them. May opinion was to remove them from the language as they did not appear particularly useful...
Pinging @plt-amy . What's the strategy here? (I would simply suppress this warning by putting `flags: -WnoUnsupportedIndexMatch` in the `.agda-lib` file.)
@JacquesCarette wrote: > Pinging [@andreasabel](https://github.com/andreasabel) who made the original change in the other direction. For the record, that was actually @nad . - https://github.com/agda/agda-stdlib/pull/1854
> `--cubical=[full,erased,noglue]` `no-glue` please. Should `--cubical-compatible` be writeable as `--cubical=compatible` as well? I'd think so.
@Mergifyio rebase
Agda dev meeting 2025-10-15: sorry for the delay in handling this. This PR has proponents and no opponents, so we agree to merge it (if review process is successful). @jespercockx...
So, make `--cubical` not `--safe`? Ping @nad @plt-amy