# Write Lean Input For Code Generation

> Learn exactly what Lean source the Proof Code Compiler accepts, download a working example zip, and structure your entry symbol correctly.

Content type: documentation
Source URL: https://www.agentpmt.com/docs/tutorials/write-lean-input-for-code-generation
Markdown URL: https://www.agentpmt.com/docs/tutorials/write-lean-input-for-code-generation?format=agent-md
Category: Tutorials

---

## Write Lean Input For Code Generation

Use 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](/marketplace/69cdb31aff055c86b8b8a224) product.

> TIP: Download A Working Example
>
> Start with the ready-to-upload example archive:
>
>   [Download the example zip](/downloads/lean-proof-code-generation-example.zip)

## What This Tool Accepts

This tool does not accept arbitrary Lean packages for whole-program compilation.
It accepts Lean source that builds a value of:

```lean
HeytingLean.LeanCP.CProgramDecl
```

The selected `entry_symbol` must elaborate to that type. The generated `c`,
`rust`, and `wasm` artifacts are emitted from that LeanCP intermediate
representation.

## What To Put In The Zip

Upload a `.zip` file whose top-level entries are Lean source files under
`UserProofs/`.

Required:

- `UserProofs/Main.lean` or another module referenced by `entry_module`
- only `.lean` files under `UserProofs/`

Do not include:

- `lakefile.lean`
- `lean-toolchain`
- `lake-manifest.json`
- `.lake/`
- external package checkouts
- generated build artifacts

> INFO: Pinned Runtime
>
> The platform supplies the pinned Lean toolchain and the pinned LeanCP runtime.
>   Your archive should only contain your own `UserProofs/` Lean source.

## How To Structure Your Lean File

Import the LeanCP declaration and syntax modules:

```lean

open HeytingLean.LeanCP
```

Your exported symbol must be a `CProgramDecl`:

```lean
def exportProgram : CProgramDecl := {
  defs := []
  main := {
    name := "add_one"
    params := [("x", .int)]
    retType := .int
    body := .ret (.binop .add (.var "x") (.intLit 1))
  }
}
```

`CProgramDecl` contains:

- `defs : List CFunDecl`
- `main : CFunDecl`

Each `CFunDecl` contains:

- `name : String`
- `params : List (String × CType)`
- `retType : CType`
- `body : CStmt`

## What Lean You Can Write

You can use ordinary Lean definitions to build your program value. It is fine
to use:

- `namespace`, `open`, `def`, and `let`
- helper functions and helper constants
- lists, tuples, and other normal Lean data needed to assemble the IR
- small amounts of proof-oriented helper code if it stays within the pinned runtime surface

What actually gets exported is only the final `CProgramDecl` value. General Lean
code is authoring support, not emitted output by itself.

## Supported Types

The exported IR currently supports these `CType` constructors:

- `.int`
- `.intSized signedness intSize`
- `.float`
- `.double`
- `.ptr ty`
- `.array ty n`
- `.funcPtr ret args`
- `.struct name`
- `.union name`
- `.enum name`
- `.typedef name`
- `.void`

In practice, the most stable surface today is:

- integers
- pointers
- fixed-size arrays
- the built-in struct layouts the runtime already knows about

## Supported Expressions

`CExpr` currently supports:

- `.var name`
- `.intLit n`
- `.floatLit v`
- `.null`
- `.sizeOf ty`
- `.cast ty expr`
- `.binop op lhs rhs`
- `.deref ptrExpr`
- `.arrayAccess arr idx`
- `.addrOf varName`
- `.fieldAccess base field`
- `.call functionName args`

Supported binary operators (`BinOp`):

- arithmetic: `.add`, `.sub`, `.mul`, `.div`, `.mod`
- comparisons: `.eq`, `.ne`, `.lt`, `.le`, `.gt`, `.ge`
- boolean or logical: `.and`, `.or`, `.lAnd`, `.lOr`
- bitwise: `.bitAnd`, `.bitOr`, `.bitXor`, `.shl`, `.shr`

## Supported Statements

`CStmt` currently supports:

- `.skip`
- `.assign lhs rhs`
- `.seq s1 s2`
- `.ite cond thenStmt elseStmt`
- `.whileInv cond invariant body`
- `.block locals body`
- `.switch expr tag caseBody defaultBody`
- `.forLoop init cond step body`
- `.break`
- `.continue`
- `.ret expr`
- `.alloc varName cellCount`
- `.free expr cellCount`
- `.decl varName ty`

Useful helper:

- `switchMany expr cases defaultStmt`

Notes:

- `whileInv` takes a loop invariant of type `HProp`. Use `HProp.htrue` when you need a permissive invariant.
- `block` takes a list of local declarations as `(String × CType)`.
- `alloc` and `free` work at the LeanCP memory-model level with explicit cell counts.

## Working Examples

### Minimal Export

```lean
def exportProgram : CProgramDecl := {
  defs := []
  main := {
    name := "add_one"
    params := [("x", .int)]
    retType := .int
    body := .ret (.binop .add (.var "x") (.intLit 1))
  }
}
```

### Simple Arithmetic Function

```lean
def applyTax : CFunDecl := {
  name := "apply_tax"
  params := [("subtotal", .int), ("tax_rate", .int)]
  retType := .int
  body := .ret
    (.binop .add
      (.var "subtotal")
      (.binop .div
        (.binop .mul (.var "subtotal") (.var "tax_rate"))
        (.intLit 100)))
}
```

### Conditional Return

```lean
def shippingProgram : CProgramDecl := {
  defs := []
  main := {
    name := "shipping_quote"
    params := [("weight_kg", .int)]
    retType := .int
    body := .ite (.binop .le (.var "weight_kg") (.intLit 5))
      (.ret (.intLit 8))
      (.ret (.intLit 15))
  }
}
```

### Loop With Invariant

```lean
def loyaltyProgram : CProgramDecl := {
  defs := []
  main := {
    name := "loyalty_points"
    params := [("orders", .int), ("points_each", .int)]
    retType := .int
    body := .block [("total", .int), ("i", .int)] (
      .seq (.assign (.var "total") (.intLit 0)) (
      .seq (.assign (.var "i") (.intLit 0)) (
      .seq (.whileInv (.binop .lt (.var "i") (.var "orders")) HProp.htrue (
          .seq (.assign (.var "total") (.binop .add (.var "total") (.var "points_each")))
               (.assign (.var "i") (.binop .add (.var "i") (.intLit 1)))))
          (.ret (.var "total")))))
  }
}
```

### Pointer And Array Access

```lean
def basketProgram : CProgramDecl := {
  defs := []
  main := {
    name := "basket_head_total"
    params := [("prices", .ptr .int)]
    retType := .int
    body := .ret (.binop .add
      (.arrayAccess (.var "prices") (.intLit 0))
      (.arrayAccess (.var "prices") (.intLit 1)))
  }
}
```

## How To Use The Example Zip

1. **Download the example archive**
   Download [lean-proof-code-generation-example.zip](/downloads/lean-proof-code-generation-example.zip).

2. **Upload it to AgentPMT**
   Use the file manager flow for the proof compiler tool so you get a `source_archive_file_id`.

3. **Call generate**
   Use `entry_module` set to `UserProofs.Main` and `entry_symbol` set to `exportProgram`.

   ```json
   {
     "action": "generate",
     "source_archive_file_id": "your_uploaded_file_id",
     "entry_module": "UserProofs.Main",
     "entry_symbol": "exportProgram",
     "target_language": "c"
   }
   ```

4. **Poll the task**
   Use `get_task` until the task reaches `completed`, then read the output artifact and bundle metadata from the result.

## What Will Not Work

These inputs are outside the supported contract:

- an `entry_symbol` whose type is not `CProgramDecl`
- a custom Lean package graph that depends on your own `lakefile.lean`
- imports that require packages not already present in the pinned runtime
- raw theorem statements with no executable `CProgramDecl`
- arbitrary Lean runtime code that is not expressed through the LeanCP IR

## Target Notes

All targets start from the same `CProgramDecl`.

- `c` is the baseline and most direct emission path
- `rust` is a deterministic translation of the same C IR and uses `unsafe` for pointer semantics
- `wasm` is the most restrictive path and should be treated as preview-grade compared with `c`

- [Proof Code Compiler Product](/marketplace/69cdb31aff055c86b8b8a224) - Open the tool in the marketplace and run generate or verify.
  - [Using Tools And Workflows](/docs/tools-and-workflows/using-tools-and-workflows) - See the broader AgentPMT tool execution flow.