search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

New Quote syntax isn't highlighted correctly in emacs #1290

Closed myreen closed 2 months ago

myreen commented 2 months ago

In emacs, End is highlighted as a keyword but Quote is not.

Quote cakeml:
  fun print_list ls =
    case ls of [] => () | (x::xs) => (print x; print_list xs)
End

This relates to #1229 and 718d989039b65d4ab82e8b979876c68c04869da1.

mn200 commented 2 months ago

Closed by aaa51b33c6c