Syntax highlighting for proof assistants

Question

In my answer to the question about the "Hello World" of proof assistants, the code is very monochromatic:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n
 

The presentation of this code on the Coq Wikipedia page isn't much better, but at least they have used green text for the word fun:

I appreciate that this is probably a longer-term feature request which won't be easy to entertain quickly, but I do think it would be nice if eventually we can get syntax highlighting working for at least the most popular theorem provers such as Coq and Lean.

Answer 1

The syntax highlighting of StackExchange markdown is based on highlight.js. Quoting from the Meta post:

Keep in mind that Stack Exchange does not maintain this syntax highlighter (aside from installing newer versions of it), and posting bug reports or feature requests concerning it here on Meta will not get them fixed or implemented.

In case you don't know, beginning a code block with three backticks and the name of your language should invoke the highlighting, if it is supported. Example:

def hello():
  return "Hello", 1 + 1

(It does not work here, if I understand it correctly. But it will on sites such as StackOverflow.)

Answer 2

As Trebor notes, StackExchange uses the external highlight.js library to do syntax highlighting. The current version of highlight.js supports Lean and Coq at least (though Lean is through an external package, so it may not be included). I don't know when these were added or if StackExchange is using that version, but it at least suggests this will be available soon, if not already. I added the coq flag to your code block to test if this will trigger yet; if not, it at least gets that code block ready for when this highlighting is available.

Once this is working and once the site has mods, tags can also have specific syntax highlighting tied to them which sets the default syntax highlighting for the question (and answers?). So they could set the default highlighting on a coq question to be Coq.