Skip to main content

All Questions

Tagged with
5 votes
1 answer
26 views

Code Reviews on topic?

There are two related questions here: Question 1: Reviewing proof scripts? I just formalized a type system in Coq (and I'm almost certain it is not "idiomatic Coq"), would it be appropriate ...
Alex Nelson's user avatar
  • 1,574
4 votes
1 answer
68 views

Policies on answers porting code

In questions such as this, the OP asks for proofs, definitions, methodology etc. on a specific topic, but does not require a specific proof assistant*. There will imaginably be answers that are purely ...
Trebor's user avatar
  • 4,025
4 votes
2 answers
107 views

Should we allow Rosetta-Stone style questions?

This question was raised in the comments of this question about idiomatic ways to prove the associativity of append. A Rosetta Stone style question would describe some kind of task in a prover-neutral ...
Greg Nisbet's user avatar
  • 3,095
13 votes
2 answers
182 views

Is this for assistants only, excluding automated provers?

Do automated theorem provers fall under the scope of this new Stack Exchange sub-site, as well as Proof Assistants?
Reubend's user avatar
  • 519