idris-hackers / software-foundations

Software Foundations in Idris
https://idris-hackers.github.io/software-foundations
MIT License
452 stars 34 forks source link

Doubles of certain special characters #5

Closed tsani closed 7 years ago

tsani commented 7 years ago

Some special characters are duplicated in the output. In particular,

Both are special in LaTeX, which is why I suspect this is happening.

yurrriq commented 7 years ago

Thanks, nice catch!