4
$\begingroup$

I am trying to understand if PA.SE is more for maths or for programming. I have a detailed question on the internals of Coq and cannot decide if to put it here or to put it in the regular stack overflow.

To give context on the exact questions (at a high level):

  1. I wanted to ask about engineering details of Coq e.g. traversing Coq terms systematically -- which is trickier than you might expect
  2. accessing the dependent type/Coq unification algorithm and the substitution/solution it outputs, likely directly in OCaml or Coq. (e.g. the apply tactic I think does it but closes goals and doesn't give me the actual substitutions for the meta-variables).

Where would these engineering questions about Coq internals go? Perhaps either is fine? I can't tell what this proof assistants SO is for exactly (yet, but really excited about it!).

$\endgroup$
4
  • 2
    $\begingroup$ I think both of these are highly on topic. $\endgroup$
    – Couchy
    Commented Jul 9, 2022 at 16:28
  • 1
    $\begingroup$ @Couchy how do I know which one is better to put it on? $\endgroup$
    – Charlie Parker
    Commented Jul 9, 2022 at 17:01
  • 1
    $\begingroup$ The distinction between what should or should not be on this site is still not clear since this site is so new. So if something is related to proof assistants in some way it should be a good match for this site. $\endgroup$
    – Couchy
    Commented Jul 9, 2022 at 18:01
  • $\begingroup$ I'd guess (on-topic) or (scope) might be suitable tags here. (Or maybe even both?) $\endgroup$
    – Martin Sleziak
    Commented Aug 13, 2022 at 12:05

1 Answer 1

Reset to default
6
$\begingroup$

My view is that we are trying to stay inclusive. This is clearly tightly related to proof assistants, and it is some of the people that hang out on this site that more likely knows the answer.

$\endgroup$

You must log in to answer this question.

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