Experimental browser for the Atmosphere
Check out these great UX improvements in Lean 4.18! ✅ New gutter decorations for errors/warnings 🔧 "Unsolved goals" markers to guide your proof 🐙 "Goals accomplished!" celebrations ▶️ Try these now in the Lean4 VSCode extension: marketplace.visualstudio.com/items?itemNa... #LeanLang #LeanProver
Apr 8, 2025, 9:32 PM
{ "uri": "at://did:plc:devnu4zs2viutk26clxykpbb/app.bsky.feed.post/3lmdgfsiqak2i", "cid": "bafyreiahma2pmush45gf275gk7zczglsseibvzceengenkrybbrx2gksdy", "value": { "text": "Check out these great UX improvements in Lean 4.18!\n\n✅ New gutter decorations for errors/warnings\n🔧 \"Unsolved goals\" markers to guide your proof\n🐙 \"Goals accomplished!\" celebrations\n\n▶️ Try these now in the Lean4 VSCode extension: marketplace.visualstudio.com/items?itemNa...\n\n#LeanLang #LeanProver", "$type": "app.bsky.feed.post", "embed": { "$type": "app.bsky.embed.images", "images": [ { "alt": "", "image": { "$type": "blob", "ref": { "$link": "bafkreibpsw7k3vd33sg7rctxxmowjtgqwv2s332o5u2gojxzfzgdulnefe" }, "mimeType": "image/jpeg", "size": 210760 }, "aspectRatio": { "width": 1148, "height": 395 } } ] }, "langs": [ "en" ], "facets": [ { "index": { "byteEnd": 287, "byteStart": 243 }, "features": [ { "uri": "https://marketplace.visualstudio.com/items?itemName=leanprover.lean4", "$type": "app.bsky.richtext.facet#link" } ] }, { "index": { "byteEnd": 298, "byteStart": 289 }, "features": [ { "tag": "LeanLang", "$type": "app.bsky.richtext.facet#tag" } ] }, { "index": { "byteEnd": 310, "byteStart": 299 }, "features": [ { "tag": "LeanProver", "$type": "app.bsky.richtext.facet#tag" } ] } ], "createdAt": "2025-04-08T21:32:38.946Z" } }