5
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ I actually read the quote you give in bullet one as "language design with focus on compiler/runtime programming/efficiency". $\endgroup$
    – Raphael Mod
    Commented 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$
    – Gilles 'SO- stop being evil' Mod
    Commented May 8, 2014 at 23:35

1 Answer 1

Reset to default
5
$\begingroup$

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).

$\endgroup$
0

You must log in to answer this question.

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