doc-gen icon indicating copy to clipboard operation
doc-gen copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Display of unit.star is glitched

Open Komyyy opened this issue 2 years ago • 1 comments

As this screenshot, display of unit.star is glitched. Screenshot_20221127-095112

OS is android.

Here is the link. matrix.pivot.list_transvec_col_mul_last_row_drop

Komyyy avatar Nov 27 '22 01:11 Komyyy

https://github.com/leanprover-community/lean/issues/789

eric-wieser avatar Jan 24 '23 15:01 eric-wieser