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
  • $\begingroup$ I actually read the quote you give in bullet one as "language design with focus on compiler/runtime programming/efficiency". $\endgroup$
    – Raphael
    May 8, 2014 at 23:02
  • $\begingroup$ @Raphael Hmmm, I guess you're right. I hadn't cottoned on “the memory sense” — I don't know what that means, but it seems to mean not the sense of small type in Coq's type theory. $\endgroup$ May 8, 2014 at 23:35

1 Answer 1


That question was pretty clearly a Coq-specific question: defining a "get n-th" function in Coq will be all but useless to a beginner in, say, Agda. How does pattern matching work in dependently typed languages would be a much better question.

Also: the Coq mailing list is really good at answering Coq-specific questions, and is appropriate, so I don't see why we should bother (though I'm sure many people here contribute to both).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .