lean4
lean4 copied to clipboard
Add `set_option pp.unicode false`
We had this option in Lean 3.