miscelleaneous

Random Lean experiments

Change easily confused diacritic to something else

Changes

1 changed files (+5/-5)