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 a porting of other answers, which I define to be an answer where no additional information (including proof-assistant-specific tricks or pitfalls) is given apart from translating the code to another proof assistant. For concreteness here's an example:
-- Agda example : (n : Nat) -> 0 + n ≡ n example n = refl
-- Idris, adapted from https://idris2.readthedocs.io/en/latest/tutorial/theorems.html example : (n:Nat) -> plus Z n = n example n = Refl
This would count as porting, unless the emphasis is on, for example, how Idris has upper-case requirements on constructors, or how Agda needs spaces around the colon, etc.
There are several options that I can think of:
- Allow this as long as the original answer is credited (according to the license of SE answers).
- Allow this, but require it to be posted as community wiki.
- Disallow this unless the port requires some degree of effort, or highlights language-specific aspects.
* The linked question is special because it is biased towards Isabelle. But there are questions like this or this.
*, but it is accidentally a valid Markdown bullet. Fixed. $\endgroup$