{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreihu4c6hfz3wthqqhy4cgkjdi24on57vebszllt7o2mqyk3fc56vpq",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjq47sfbl6a2"
  },
  "path": "/t/lawvere-theories/13944#post_6",
  "publishedAt": "2026-04-17T22:38:29.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "By the way, does the GHC type checker know the principle of induction? Say we have\n\n\n    data Peano = Zero | Succ Peano\n    class Prop (n :: Peano)\n\n\nNow suppose I have implemented\n\n\n    instance Prop Zero\n    instance (Prop n) => Prop (Succ n)\n\n\nCan I then use the universally quantified constraint\n\n\n    forall n. Prop n\n\n\nin my contexts?",
  "title": "Lawvere theories"
}