Policies on answers porting code

Question

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.

Answer 1

When a piece of concrete code makes a good answer, and the question is fully proof-assistant-agnostic, then porting such a piece of code to other proof assistants makes sense (it adds value for future readers who are interested in the question and know a specific proof assistant but not others).

I don't think such ports should be always posted as CW, since being able to port some code in one PA into another is no easy feat in general IMO. For trivial cases like the Agda-Idris example in the question, it makes sense to create a CW answer collecting multiple ports of the given code.