{
  "schema_version": "agentpmt.docs.v1",
  "generated_at": "2026-07-23T23:22:04.920Z",
  "release_id": "9bd28307d3dc8ff05bcac2f755a96681a9e650091caba4ab5ecbd5a1d6d62acc",
  "id": "69d13e0f2117cce34a638557",
  "page_url": "https://www.agentpmt.com/docs/workflow-authoring/write-lean-input-for-code-generation",
  "markdown_url": "https://www.agentpmt.com/docs/workflow-authoring/write-lean-input-for-code-generation?format=agent-md",
  "json_url": "https://www.agentpmt.com/docs/workflow-authoring/write-lean-input-for-code-generation?format=agent-json",
  "source_path": "content/docs/write-lean-input-for-code-generation.mdoc",
  "updated_at": "2026-04-30T16:00:29.000Z",
  "headings": [
    {
      "depth": 2,
      "id": "what-this-tool-accepts",
      "title": "What This Tool Accepts"
    },
    {
      "depth": 2,
      "id": "what-to-put-in-the-zip",
      "title": "What To Put In The Zip"
    },
    {
      "depth": 2,
      "id": "how-to-structure-your-lean-file",
      "title": "How To Structure Your Lean File"
    },
    {
      "depth": 2,
      "id": "what-lean-you-can-write",
      "title": "What Lean You Can Write"
    },
    {
      "depth": 2,
      "id": "supported-types",
      "title": "Supported Types"
    },
    {
      "depth": 2,
      "id": "supported-expressions",
      "title": "Supported Expressions"
    },
    {
      "depth": 2,
      "id": "supported-statements",
      "title": "Supported Statements"
    },
    {
      "depth": 2,
      "id": "working-examples",
      "title": "Working Examples"
    },
    {
      "depth": 3,
      "id": "minimal-export",
      "title": "Minimal Export"
    },
    {
      "depth": 3,
      "id": "simple-arithmetic-function",
      "title": "Simple Arithmetic Function"
    },
    {
      "depth": 3,
      "id": "conditional-return",
      "title": "Conditional Return"
    },
    {
      "depth": 3,
      "id": "loop-with-invariant",
      "title": "Loop With Invariant"
    },
    {
      "depth": 3,
      "id": "pointer-and-array-access",
      "title": "Pointer And Array Access"
    },
    {
      "depth": 2,
      "id": "how-to-use-the-example-zip",
      "title": "How To Use The Example Zip"
    },
    {
      "depth": 2,
      "id": "what-will-not-work",
      "title": "What Will Not Work"
    },
    {
      "depth": 2,
      "id": "target-notes",
      "title": "Target Notes"
    }
  ],
  "related_products": [
    "69cdb31aff055c86b8b8a224"
  ],
  "related_workflows": [],
  "doc": {
    "title": "Write Lean Input For Code Generation",
    "description": "Learn exactly what Lean source the Proof Code Compiler accepts, download a working example zip, and structure your entry symbol correctly.",
    "category": "Workflow Authoring",
    "image": null,
    "full_path": "workflow-authoring/write-lean-input-for-code-generation",
    "body_markdown": "# Write Lean Input For Code Generation\n\nUse this guide when you want to convert Lean code into `c`, `rust`, or `wasm` with the [Lean To Code Translator W Proof  - C Rust Wasm](https://www.agentpmt.com/marketplace/69cdb31aff055c86b8b8a224) product.\n\n**Download A Working Example**\n\nStart with the ready-to-upload example archive:\n\n[Download the example zip](https://www.agentpmt.com/docs-assets/downloads/lean-proof-code-generation-example.zip)\n\n## What This Tool Accepts\n\nThis tool does not accept arbitrary Lean packages for whole-program compilation.\nIt accepts Lean source that builds a value of:\n\n```lean\nHeytingLean.LeanCP.CProgramDecl\n```\n\nThe selected `entry_symbol` must elaborate to that type. The generated `c`,\n`rust`, and `wasm` artifacts are emitted from that LeanCP intermediate\nrepresentation.\n\n## What To Put In The Zip\n\nUpload a `.zip` file whose top-level entries are Lean source files under\n`UserProofs/`.\n\nRequired:\n\n- `UserProofs/Main.lean` or another module referenced by `entry_module`\n- only `.lean` files under `UserProofs/`\n\nDo not include:\n\n- `lakefile.lean`\n- `lean-toolchain`\n- `lake-manifest.json`\n- `.lake/`\n- external package checkouts\n- generated build artifacts\n\n**Pinned Runtime**\n\nThe platform supplies the pinned Lean toolchain and the pinned LeanCP runtime.\nYour archive should only contain your own `UserProofs/` Lean source.\n\n## How To Structure Your Lean File\n\nImport the LeanCP declaration and syntax modules:\n\n```lean\nimport HeytingLean.LeanCP.Lang.CDecl\nimport HeytingLean.LeanCP.Lang.CSyntax\nimport HeytingLean.LeanCP.Core.HProp\n\nopen HeytingLean.LeanCP\n```\n\nYour exported symbol must be a `CProgramDecl`:\n\n```lean\ndef exportProgram : CProgramDecl := {\n  defs := []\n  main := {\n    name := \"add_one\"\n    params := [(\"x\", .int)]\n    retType := .int\n    body := .ret (.binop .add (.var \"x\") (.intLit 1))\n  }\n}\n```\n\n`CProgramDecl` contains:\n\n- `defs : List CFunDecl`\n- `main : CFunDecl`\n\nEach `CFunDecl` contains:\n\n- `name : String`\n- `params : List (String × CType)`\n- `retType : CType`\n- `body : CStmt`\n\n## What Lean You Can Write\n\nYou can use ordinary Lean definitions to build your program value. It is fine\nto use:\n\n- `namespace`, `open`, `def`, and `let`\n- helper functions and helper constants\n- lists, tuples, and other normal Lean data needed to assemble the IR\n- small amounts of proof-oriented helper code if it stays within the pinned runtime surface\n\nWhat actually gets exported is only the final `CProgramDecl` value. General Lean\ncode is authoring support, not emitted output by itself.\n\n## Supported Types\n\nThe exported IR currently supports these `CType` constructors:\n\n- `.int`\n- `.intSized signedness intSize`\n- `.float`\n- `.double`\n- `.ptr ty`\n- `.array ty n`\n- `.funcPtr ret args`\n- `.struct name`\n- `.union name`\n- `.enum name`\n- `.typedef name`\n- `.void`\n\nIn practice, the most stable surface today is:\n\n- integers\n- pointers\n- fixed-size arrays\n- the built-in struct layouts the runtime already knows about\n\n## Supported Expressions\n\n`CExpr` currently supports:\n\n- `.var name`\n- `.intLit n`\n- `.floatLit v`\n- `.null`\n- `.sizeOf ty`\n- `.cast ty expr`\n- `.binop op lhs rhs`\n- `.deref ptrExpr`\n- `.arrayAccess arr idx`\n- `.addrOf varName`\n- `.fieldAccess base field`\n- `.call functionName args`\n\nSupported binary operators (`BinOp`):\n\n- arithmetic: `.add`, `.sub`, `.mul`, `.div`, `.mod`\n- comparisons: `.eq`, `.ne`, `.lt`, `.le`, `.gt`, `.ge`\n- boolean or logical: `.and`, `.or`, `.lAnd`, `.lOr`\n- bitwise: `.bitAnd`, `.bitOr`, `.bitXor`, `.shl`, `.shr`\n\n## Supported Statements\n\n`CStmt` currently supports:\n\n- `.skip`\n- `.assign lhs rhs`\n- `.seq s1 s2`\n- `.ite cond thenStmt elseStmt`\n- `.whileInv cond invariant body`\n- `.block locals body`\n- `.switch expr tag caseBody defaultBody`\n- `.forLoop init cond step body`\n- `.break`\n- `.continue`\n- `.ret expr`\n- `.alloc varName cellCount`\n- `.free expr cellCount`\n- `.decl varName ty`\n\nUseful helper:\n\n- `switchMany expr cases defaultStmt`\n\nNotes:\n\n- `whileInv` takes a loop invariant of type `HProp`. Use `HProp.htrue` when you need a permissive invariant.\n- `block` takes a list of local declarations as `(String × CType)`.\n- `alloc` and `free` work at the LeanCP memory-model level with explicit cell counts.\n\n## Working Examples\n\n### Minimal Export\n\n```lean\ndef exportProgram : CProgramDecl := {\n  defs := []\n  main := {\n    name := \"add_one\"\n    params := [(\"x\", .int)]\n    retType := .int\n    body := .ret (.binop .add (.var \"x\") (.intLit 1))\n  }\n}\n```\n\n### Simple Arithmetic Function\n\n```lean\ndef applyTax : CFunDecl := {\n  name := \"apply_tax\"\n  params := [(\"subtotal\", .int), (\"tax_rate\", .int)]\n  retType := .int\n  body := .ret\n    (.binop .add\n      (.var \"subtotal\")\n      (.binop .div\n        (.binop .mul (.var \"subtotal\") (.var \"tax_rate\"))\n        (.intLit 100)))\n}\n```\n\n### Conditional Return\n\n```lean\ndef shippingProgram : CProgramDecl := {\n  defs := []\n  main := {\n    name := \"shipping_quote\"\n    params := [(\"weight_kg\", .int)]\n    retType := .int\n    body := .ite (.binop .le (.var \"weight_kg\") (.intLit 5))\n      (.ret (.intLit 8))\n      (.ret (.intLit 15))\n  }\n}\n```\n\n### Loop With Invariant\n\n```lean\ndef loyaltyProgram : CProgramDecl := {\n  defs := []\n  main := {\n    name := \"loyalty_points\"\n    params := [(\"orders\", .int), (\"points_each\", .int)]\n    retType := .int\n    body := .block [(\"total\", .int), (\"i\", .int)] (\n      .seq (.assign (.var \"total\") (.intLit 0)) (\n      .seq (.assign (.var \"i\") (.intLit 0)) (\n      .seq (.whileInv (.binop .lt (.var \"i\") (.var \"orders\")) HProp.htrue (\n          .seq (.assign (.var \"total\") (.binop .add (.var \"total\") (.var \"points_each\")))\n               (.assign (.var \"i\") (.binop .add (.var \"i\") (.intLit 1)))))\n          (.ret (.var \"total\")))))\n  }\n}\n```\n\n### Pointer And Array Access\n\n```lean\ndef basketProgram : CProgramDecl := {\n  defs := []\n  main := {\n    name := \"basket_head_total\"\n    params := [(\"prices\", .ptr .int)]\n    retType := .int\n    body := .ret (.binop .add\n      (.arrayAccess (.var \"prices\") (.intLit 0))\n      (.arrayAccess (.var \"prices\") (.intLit 1)))\n  }\n}\n```\n\n## How To Use The Example Zip\n\n### Download the example archive\n\nDownload [lean-proof-code-generation-example.zip](https://www.agentpmt.com/docs-assets/downloads/lean-proof-code-generation-example.zip).\n\n### Upload it to AgentPMT\n\nUse the file manager flow for the proof compiler tool so you get a `source_archive_file_id`.\n\n### Call generate\n\nUse `entry_module` set to `UserProofs.Main` and `entry_symbol` set to `exportProgram`.\n\n```json\n{\n  \"action\": \"generate\",\n  \"source_archive_file_id\": \"your_uploaded_file_id\",\n  \"entry_module\": \"UserProofs.Main\",\n  \"entry_symbol\": \"exportProgram\",\n  \"target_language\": \"c\"\n}\n```\n\n### Poll the task\n\nUse `get_task` until the task reaches `completed`, then read the output artifact and bundle metadata from the result.\n\n## What Will Not Work\n\nThese inputs are outside the supported contract:\n\n- an `entry_symbol` whose type is not `CProgramDecl`\n- a custom Lean package graph that depends on your own `lakefile.lean`\n- imports that require packages not already present in the pinned runtime\n- raw theorem statements with no executable `CProgramDecl`\n- arbitrary Lean runtime code that is not expressed through the LeanCP IR\n\n## Target Notes\n\nAll targets start from the same `CProgramDecl`.\n\n- `c` is the baseline and most direct emission path\n- `rust` is a deterministic translation of the same C IR and uses `unsafe` for pointer semantics\n- `wasm` is the most restrictive path and should be treated as preview-grade compared with `c`\n\n### [Proof Code Compiler Product](https://www.agentpmt.com/marketplace/69cdb31aff055c86b8b8a224)\n\nOpen the tool in the marketplace and run generate or verify.\n\n### [Using Tools And Workflows](https://www.agentpmt.com/docs/getting-started/using-workflows-and-tools)\n\nSee the broader AgentPMT tool execution flow.\n"
  }
}