Fix LaTeX not escaping properly in L12_Insert.lean

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Closed tautastic closed 4 months ago

tautastic commented 4 months ago

Same problem in Game/Levels/Sum/L01_Simp.lean.

joneugster commented 4 months ago

Danke!