{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreic24egp3zt2q2cykstk2fmfbvwrg6fr7zl5qazsnom7vnjeexf7qu",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mltqpllmlmb2"
  },
  "path": "/t/knownnat-indexed-vectors/14099?page=2#post_25",
  "publishedAt": "2026-05-14T19:31:34.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "checked-literals plugin"
  ],
  "textContent": "I meant mainly for the use of `fromInteger`, to avoid explicitly converting to `Finite` each time one wants to index the vector. Also given a known `Nat` the compiler should be able to produce a warning/error if a literal falls outside of the `Finite` bounds, similarly to the checked-literals plugin. Right now using `Finite` types is too clumsy.",
  "title": "KnownNat-indexed vectors"
}