Zulip Chat Archive

Stream: lean4

Topic: guard widgets

Patrick Massot (Feb 19 2025 at 12:55):

Do we have a version of #guard_msgs that would check the displayed widget text?

Patrick Massot (Feb 19 2025 at 12:59):

Context at #22077

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Feb 19 2025 at 19:24):

I don't know of such a thing, but you could conceivably write a command that inspects the InfoTree, retrieves the widget prop JSON stored therein, and runs tests on that JSON.

Last updated: May 02 2025 at 03:31 UTC