ATProto Browser

ATProto Browser

Experimental browser for the Atmosphere

Post

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

Record data

{
  "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"
  }
}