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 product.

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:

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

How To Structure Your Lean File

Import the LeanCP declaration and syntax modules:

import HeytingLean.LeanCP.Lang.CDecl
import HeytingLean.LeanCP.Lang.CSyntax
import HeytingLean.LeanCP.Core.HProp

open HeytingLean.LeanCP

Your exported symbol must be a CProgramDecl:

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

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

Simple Arithmetic Function

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

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

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

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

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

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