search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Warning: Unexpected token during syntax-highlighting: '₁' #29

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago 
!! Warning: Unexpected token during syntax-highlighting: '₁'
!! Alectryon's lexer isn't perfect: please send us an example.
!! Context:
        forall x y : A s,
        cong_ker f s x y ->
        (f s x; ❘ (x; 1) ❘₋₁

https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2352

cpitclaudel commented 3 years ago

Yup, I think we won't really be able to fix this — notations can contain arbitrary sequences, basically, so the best might just be to turn that warning off and wait until Coq can do the fontification for us.