ATProto Browser

Record data

{
  "uri": "at://did:plc:devnu4zs2viutk26clxykpbb/app.bsky.feed.post/3lke2cps3622v",
  "cid": "bafyreihpzqub2n2su2z6zyd4m3m2di2m24fbduvd34d2jhj4bih5z7vtiq",
  "value": {
    "text": "The type of refl is inferred as refl.{u_1} {x+ : Sort u_1} {x : x+} : x = x. In these kinds of \"iterated\" implicit parameters, we only display those for which we have an actual name that occurs in the source code. This is why x is displayed, but its type (x+) is not.",
    "$type": "app.bsky.feed.post",
    "langs": [
      "en"
    ],
    "reply": {
      "root": {
        "cid": "bafyreidw43i2hmxbnjsvr6qzis4enpy7w5x5hv2eusaxfn2x76affqx7ae",
        "uri": "at://did:plc:devnu4zs2viutk26clxykpbb/app.bsky.feed.post/3lkbqxptkwc24"
      },
      "parent": {
        "cid": "bafyreifp6pcksmvnkm5alm3et5pkkltabbdnay24mulkxfgi7lzdg5ybfu",
        "uri": "at://did:plc:ibpuvdpgd3pbwczlg3gynyaw/app.bsky.feed.post/3lkdlstht6k2q"
      }
    },
    "createdAt": "2025-03-14T16:38:27.025Z"
  }
}