# C Cpp To Lean4 Translator

> Translate C or C++ programs into equivalent Lean4 code, preserving program semantics and ensuring the generated code is well-typed, executable, and can run successfully. Use when the user asks to convert C/C++ code to Lean4, port C/C++ programs to Lean4, translate imperative code to functional Lean4, or create Lean4 versions of C/C++ algorithms.

- **Type:** Skill
- **Install:** `agentstack add skill-arabelatso-skills-4-se-c-cpp-to-lean4-translator`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ArabelaTso](https://agentstack.voostack.com/s/arabelatso)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/c-cpp-to-lean4-translator
- **Website:** https://ArabelaTso.github.io/Skills-4-SE/

## Install

```sh
agentstack add skill-arabelatso-skills-4-se-c-cpp-to-lean4-translator
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# C/C++ to Lean4 Translator

## Overview

Transform C or C++ programs into equivalent Lean4 code that preserves the original semantics while leveraging Lean4's functional programming paradigm, strong type system, and proof capabilities.

## Translation Workflow

### Step 1: Analyze Input Code

Understand the C/C++ program structure and semantics:

1. **Identify program components:**
   - Functions and their signatures
   - Data structures (structs, classes, arrays)
   - Control flow patterns (loops, conditionals)
   - Memory management (allocation, pointers)
   - I/O operations
   - Dependencies and includes

2. **Understand semantics:**
   - What does the program compute?
   - What are the inputs and outputs?
   - Are there side effects?
   - What are the invariants and preconditions?

3. **Note translation challenges:**
   - Pointer arithmetic
   - Mutable state
   - Imperative loops
   - Manual memory management
   - Undefined behavior

### Step 2: Design Lean4 Structure

Plan the Lean4 equivalent before writing code:

1. **Choose appropriate types:**
   - `Int` for signed integers
   - `Nat` for unsigned integers and array indices
   - `Float` for floating-point numbers
   - `Array` for dynamic arrays
   - `List` for linked lists
   - Custom `structure` types for structs/classes

2. **Determine purity:**
   - Pure functions: return values directly
   - Side effects: use `IO` monad
   - Mutable state: use `IO.Ref` or `ST` monad

3. **Plan control flow translation:**
   - Loops → Recursive functions
   - Mutable variables → Function parameters
   - Early returns → Conditional expressions

4. **Handle memory:**
   - Stack allocation → Direct values
   - Heap allocation → Automatic memory management
   - Pointers → Direct values or references

### Step 3: Translate Code

Follow these translation principles:

#### Functions

**Pattern: Pure function**
```c
// C/C++
int add(int a, int b) {
    return a + b;
}
```

```lean
-- Lean4
def add (a b : Int) : Int :=
  a + b
```

**Pattern: Function with side effects**
```c
// C/C++
void printSum(int a, int b) {
    printf("%d\n", a + b);
}
```

```lean
-- Lean4
def printSum (a b : Int) : IO Unit :=
  IO.println (a + b)
```

#### Control Flow

**Pattern: If-else**
```c
// C/C++
int max(int a, int b) {
    if (a > b) return a;
    else return b;
}
```

```lean
-- Lean4
def max (a b : Int) : Int :=
  if a > b then a else b
```

**Pattern: For loop → Tail recursion**
```c
// C/C++
int sum(int n) {
    int result = 0;
    for (int i = 0; i = n then acc
    else loop (i + 1) (acc + i)
  loop 0 0
```

**Pattern: While loop → Recursion**
```c
// C/C++
int factorial(int n) {
    int result = 1;
    while (n > 1) {
        result *= n;
        n--;
    }
    return result;
}
```

```lean
-- Lean4
def factorial (n : Nat) : Nat :=
  let rec loop (n acc : Nat) : Nat :=
    if n  max) {
            max = arr[i];
        }
    }
    return max;
}
```

**Lean4 Output:**
```lean
def findMax (arr : Array Int) : Option Int :=
  if arr.isEmpty then
    none
  else
    some (arr.foldl max arr[0]!)
```

### Example 3: Struct with Methods

**C/C++ Input:**
```cpp
struct Rectangle {
    int width;
    int height;

    int area() {
        return width * height;
    }

    int perimeter() {
        return 2 * (width + height);
    }
};
```

**Lean4 Output:**
```lean
structure Rectangle where
  width : Nat
  height : Nat
  deriving Repr

def Rectangle.area (r : Rectangle) : Nat :=
  r.width * r.height

def Rectangle.perimeter (r : Rectangle) : Nat :=
  2 * (r.width + r.height)
```

### Example 4: I/O Program

**C/C++ Input:**
```c
#include 

int main() {
    int n;
    printf("Enter a number: ");
    scanf("%d", &n);
    printf("Factorial: %d\n", factorial(n));
    return 0;
}
```

**Lean4 Output:**
```lean
def factorial (n : Nat) : Nat :=
  if n >= (·.getLine)
  match input.trim.toNat? with
  | some n =>
    IO.println s!"Factorial: {factorial n}"
  | none =>
    IO.println "Invalid input"
```

## Best Practices

1. **Start simple:** Translate basic functions first, then build up complexity
2. **Preserve semantics:** Ensure the Lean4 code computes the same results
3. **Use types wisely:** Leverage Lean4's type system for correctness
4. **Embrace immutability:** Prefer pure functions over mutable state
5. **Test thoroughly:** Verify outputs match for various inputs
6. **Document assumptions:** Note any semantic differences or limitations
7. **Leverage standard library:** Use built-in functions when available
8. **Handle errors gracefully:** Use `Option` or `Except` for error cases

## Limitations and Considerations

1. **Undefined behavior:** C/C++ undefined behavior must be handled explicitly in Lean4
2. **Performance:** Functional code may have different performance characteristics
3. **Concurrency:** C/C++ threading requires different approaches in Lean4
4. **Low-level operations:** Bit manipulation and pointer arithmetic need careful translation
5. **External libraries:** C/C++ library calls may not have direct Lean4 equivalents
6. **Macros:** C preprocessor macros need manual translation
7. **Templates:** C++ templates translate to Lean4 generics differently

## Resources

- **Translation patterns:** See [translation_patterns.md](references/translation_patterns.md) for comprehensive pattern catalog
- **Lean4 documentation:** https://lean-lang.org/documentation/
- **Lean4 standard library:** https://github.com/leanprover/lean4/tree/master/src/Init

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [ArabelaTso](https://github.com/ArabelaTso)
- **Source:** [ArabelaTso/Skills-4-SE](https://github.com/ArabelaTso/Skills-4-SE)
- **License:** Apache-2.0
- **Homepage:** https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-arabelatso-skills-4-se-c-cpp-to-lean4-translator
- Seller: https://agentstack.voostack.com/s/arabelatso
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.