We raised the issue of scope limits for proof assistants a while ago, and didn't come to a conclusion. It's been two years, what does the community think now?
More specifically, is the question Coq: default values for vectors on-topic? It combines several aspects:
- language design with a strong theoretic underpinning (“Was this built this way to keep the type small”)
- type theory — although not explicitly formulated in the question, the answer would involve some
- library design
- programming in a proof assistant language