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-translator89
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/skillValidation for skill structure
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines a specific translation task between C/C++ and Lean4. It provides comprehensive trigger terms covering natural variations users might use, includes an explicit 'Use when' clause with multiple scenarios, and occupies a distinctive niche that minimizes conflict risk with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Translate C or C++ programs into equivalent Lean4 code', 'preserving program semantics', 'ensuring the generated code is well-typed, executable, and can run successfully'. These are concrete, actionable capabilities. | 3 / 3 |
Completeness | Clearly answers both what (translate C/C++ to Lean4 with semantic preservation and type safety) AND when (explicit 'Use when' clause with four specific trigger scenarios). The 'Use when...' clause is present and comprehensive. | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms users would say: 'convert C/C++ code to Lean4', 'port C/C++ programs', 'translate imperative code to functional Lean4', 'Lean4 versions of C/C++ algorithms'. Covers multiple phrasings (convert, port, translate) and both language names. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche combining two specific languages (C/C++ and Lean4). The combination of source language (C/C++) and target language (Lean4) creates a very narrow, clear scope unlikely to conflict with other translation or code skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
72%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a well-structured translation skill with excellent actionability through concrete, executable code examples covering the major C/C++ to Lean4 translation patterns. The main weaknesses are moderate verbosity in the workflow description (explaining analysis steps Claude would naturally perform) and insufficient validation/error recovery guidance for when translations fail to type-check or produce incorrect results.
Suggestions
Add explicit validation checkpoints with error recovery guidance, e.g., 'If type error occurs: check integer signedness, verify array bounds handling, ensure Option types are handled'
Condense Steps 1-2 (Analyze and Design) into a brief checklist rather than detailed explanations of what to look for - Claude knows how to analyze code
Add a troubleshooting section for common Lean4 type errors that arise during translation (e.g., termination proofs, decidability requirements)
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The skill is reasonably efficient but includes some unnecessary explanation (e.g., 'Understand the C/C++ program structure and semantics' section explains analysis steps Claude would naturally perform). The translation patterns and examples are valuable, but the workflow steps could be more condensed. | 2 / 3 |
Actionability | Excellent actionability with fully executable code examples for every translation pattern. The C/C++ to Lean4 mappings are concrete, copy-paste ready, and cover a comprehensive range of patterns including functions, control flow, data structures, and I/O. | 3 / 3 |
Workflow Clarity | The 6-step workflow is clearly sequenced, but validation is weak. Step 5 mentions 'lake build' and #eval testing, but lacks explicit validation checkpoints or feedback loops for catching translation errors. No guidance on what to do when type errors occur or how to debug failed translations. | 2 / 3 |
Progressive Disclosure | Good structure with clear overview, detailed patterns inline (appropriate for a translation skill), and references to external files for comprehensive pattern catalogs. The quick reference table provides excellent at-a-glance navigation. References are one level deep and clearly signaled. | 3 / 3 |
Total | 10 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
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.