Andreas Abel

Rebasing this on master... This might fix the CI failure.

> Related: #4526. Some suggestions from that ticket that weren't implemented: > > * Add a `.agda-lib` file for the builtin modules. This could likely be done right away. >...

Here is a similar case, with elimination from a `Prop`: ```agda {-# OPTIONS --prop --cumulativity #-} open import Agda.Builtin.Bool data Foo : Prop where tt ff : Foo Boo :...

@WhatisRT : How do you propose scope-checking would work then? The problem we are facing here is that the scope-checker needs to know about the names and their kinds (module,...

Shrinking away the universe-polymorphism: ```agda open import Agda.Builtin.Equality open import Agda.Builtin.Nat open import Agda.Builtin.List data Fin : Nat → Set where zero : ∀ {n} → Fin (suc n) suc...

Shrinking the Table away: ```agda open import Agda.Builtin.Equality open import Agda.Builtin.Nat open import Agda.Builtin.List data Fin : Nat → Set where zero : ∀ {n} → Fin (suc n) suc...

Welcome to supplement the documentation!, here: https://github.com/agda/agda/blob/505464961f07f0991263708fd8cbf5f7ad12f53f/doc/user-manual/language/lambda-abstraction.lagda.rst#L16-L19

Thanks for investigating. The individual items would be more valuable with reproducers (although I think you couldn't pin performance problems to just one of these items, esp. when the problem...

Not sure about `dlist`. They are good for construction, but as soon as you start consuming, they need to be collapsed into ordinary lists. If you store a `dlist`, then...

(Removing label "bug": There is no evidence for such claim here.)