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

Published 20 hours ago • verified publisher icon leanprover

LeanInk: Pretty rendering

Open hargoniX opened this issue 2 years ago • 1 comments

Alectryon can render pretty versions of data structures like rbtrees, integrating this feature from the compiler: https://github.com/leanprover/lean4/pull/1238 might allow us to do the same (https://alectryon-paper.github.io/snippets/rbt.html)

hargoniX avatar Jun 23 '22 23:06 hargoniX

yes this is exactly a use case of the user-widgets feature

EdAyers avatar Jun 24 '22 13:06 EdAyers

Won't implement, we have Verso.

hargoniX avatar Jun 09 '24 21:06 hargoniX