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.

Install with Tessl CLI

npx tessl i github:ArabelaTso/Skills-4-SE --skill c-cpp-to-lean4-translator

What are skills?

Review — 86%

Does it follow best practices?

If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:

npx tessl skill review --optimize ./path/to/skill

Learn more

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

Evaluation results

94%

Geometric Shapes Library Port

Struct and method translation

Criteria

Without context

With context

structure keyword

100%

deriving Repr

100%

Nat for non-negative fields

62%

100%

Float for floating-point

100%

Method naming convention

100%

Option for fallible ops

70%

100%

Pure functions without IO

100%

Array over List

100%

Doc comments

100%

Standard library idioms

30%

40%

eval test expressions

100%

Without context: $0.1923 · 2m 5s · 8 turns · 13 in / 4,380 out tokens

With context: $0.4383 · 3m 35s · 21 turns · 321 in / 5,562 out tokens

72%

Statistics Utility Port

Loop and control flow patterns

Criteria

Without context

With context

let rec loop pattern

66%

Tail recursion for loops

100%

match for switch/case

100%

Safe array access

100%

Nat for array indices

37%

87%

foldl over manual accumulation

100%

Pattern matching over if-else chains

20%

100%

Pure functions without IO

100%

Nat vs Int type choice

62%

75%

eval test expressions

100%

Without context: $0.1956 · 2m 4s · 12 turns · 19 in / 2,693 out tokens

With context: $0.6004 · 4m 29s · 20 turns · 29 in / 10,031 out tokens

97%

Interactive Number Utilities Port

IO, pointers, and error handling

Criteria

Without context

With context

IO monad for side effects

100%

do notation for sequencing

100%

IO.println for printf

62%

String interpolation syntax

100%

Pointer params as return values

100%

Tuple for multiple returns

100%

Option for NULL/sentinel

100%

stdin reading pattern

80%

100%

No manual memory management

100%

eval test expressions

100%

Explicit type conversion

75%

100%

Without context: $0.2410 · 2m 5s · 12 turns · 19 in / 3,975 out tokens

With context: $0.5412 · 3m 40s · 18 turns · 4,778 in / 6,392 out tokens

Evaluated: about 11 hours ago
Agent: Claude Code

Table of Contents

Geometric Shapes Library Port Statistics Utility Port Interactive Number Utilities Port

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.