Agent skill

Vero Lean Pitfalls

Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation).

Apache-2.0Auto-check: notesWriting & Content

Install Vero Lean Pitfalls

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .claude/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .claude/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Paste into Claude Code

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .claude/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .agents/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .agents/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .agents/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .cursor/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .cursor/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/sunblaze-ucb/vero.git --path .claude/skills/vero-lean-pitfalls

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .gemini/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .gemini/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .github/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .github/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .github/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-lean-pitfalls --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/.claude/skills/vero-lean-pitfalls .opencode/skills/vero-lean-pitfalls && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "vero-lean-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-lean-pitfalls into .opencode/skills/vero-lean-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-lean-pitfalls", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: vero-lean-pitfalls
GitHub stars: 107
Token cost: ~1.4k tokens
SKILL.md length: 555 words
Files: 1
Skills in repo: 16
Repo updated: Aug 17, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation).

Works in 10 steps: noncomputable Propagation → Standard Library Mappings → Prop vs Bool Confusion → …
Tasks that involve Translation
SKILL.md covers 1. noncomputable Propagation, 2. Standard Library Mappings, 3. Prop vs Bool Confusion and 4. Natural Number Subtraction, plus 6 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Vero Lean Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation). Pair with vero-translate.

Its SKILL.md is about 1.4k tokens, which your agent loads only when the skill is triggered. It is a single SKILL.md file with no bundled scripts.

It sits in Writing & Content, covering Translation. The licence is Apache-2.0.

When your agent uses it

Tasks that involve Translation

Example prompts

“/vero-lean-pitfalls”

Requirements

Pre-approved tools (allowed-tools): Read, Write, Edit, Bash, Grep, Glob

Workflow steps

10 steps, taken from the step headings in SKILL.md.

noncomputable Propagation
Standard Library Mappings
Prop vs Bool Confusion
Natural Number Subtraction
Division by Zero
Import Order
autoImplicit Pitfalls
deriving Clause Limitations
Mutual Recursion
Universe Polymorphism

What it can do on your machine

Read from SKILL.md and the folder at commit 0a7325d. It shows what the files ask for, not the result of running them.

Tool permissions
Pre-approves these tools, so the agent can use them without asking each time:
- Read
- Write
- Edit
- Bash
- Grep
- Glob
From allowed-tools in the SKILL.md frontmatter.
Runs code
No scripts in the folder and no shell commands in SKILL.md (its code samples are lean and bash).
From the folder's file list and the shell code blocks in SKILL.md.
Network
No URLs in SKILL.md.
From URLs in SKILL.md, links to its own repository left out.
Credentials
Names no API keys, tokens, secrets or passwords.
From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Vero Lean Pitfalls loads about 1.4k tokens when it runs. Until then it costs about 44 tokens; SKILL.md has 555 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it: ~44
When it runs · the whole SKILL.md, loaded when a task matches: ~1.4k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check: notes

The automated check noted patterns worth knowing about, such as sudo or a known installer.

NotePre-approves every shell command (allowed-tools: Bash)SKILL.md
```
allowed-tools: Read, Write, Edit, Bash, Grep, Glob
```

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from sunblaze-ucb/vero at commit 0a7325d, republished under its Apache-2.0 licence (© sunblaze-ucb). 555 words, ~1,371 tokens.

Download SKILL.mdSave it as .claude/skills/vero-lean-pitfalls/SKILL.md (or your agent's skills folder).

name: vero-lean-pitfalls
description: Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation). Pair with vero-translate.
allowed-tools: Read, Write, Edit, Bash, Grep, Glob

Lean 4 Translation Pitfalls

Common issues encountered when translating formally-verified code from Dafny, Verus, or Coq into Lean 4. Check each pitfall proactively during translation to avoid discovering them only at build time.

1. noncomputable Propagation

Problem: When a type or function is declared opaque in Lean (because the source marks it as external/FFI), any function that references it becomes non-computable. Lean requires these to be explicitly marked noncomputable. This propagates transitively through the call chain.

Symptom:

error: definition 'funcName' depends on opaque 'externalFunc'

Fix: Add noncomputable to the definition:

lean

noncomputable def funcName (x : T) : U := ...

Prevention: After declaring any opaque, immediately grep for all functions that reference it and proactively add noncomputable:

bash

grep -rn 'opaqueName' ProjectName/ --include='*.lean'

Key insight: noncomputable only matters for definitions that Lean tries to compile to executable code. Theorems and proofs don't need it. #guard tests CANNOT use noncomputable definitions — you need executable reference implementations in the Test file.

2. Standard Library Mappings

Before declaring anything as opaque, check if Lean's stdlib already provides it. Use lean_local_search MCP tool if available.

Source construct	Lean equivalent
HashMap/Dictionary	`Std.HashMap K V`
HashSet	`Std.HashSet T`
Dynamic array / Vec	`Array T`
Linked list	`List T`
Optional/Option	`Option T`
Result/Either	`Except E T`
Tuple	`T × U` or `Prod T U`
String	`String`
Byte array	`ByteArray`
Integer (unbounded)	`Int`
Natural number	`Nat`
Bitvector	`BitVec n`

3. Prop vs Bool Confusion

Problem: Lean distinguishes Prop (logical propositions) from Bool (computational booleans). Source languages often conflate these.

Rules:

Specifications and theorem statements use Prop
Computable functions that branch use Bool
Decidable instances bridge the gap (use decide to go from Prop to Bool)
#guard requires Bool or Decidable — cannot test arbitrary Prop

Common fix: If a spec function returns Bool but should be Prop, change the return type and use := with propositional connectives:

lean

-- Bad: def spec (x : Nat) : Bool := x > 0 && x < 10
-- Good: def spec (x : Nat) : Prop := x > 0 ∧ x < 10

4. Natural Number Subtraction

Problem: In Lean, Nat subtraction is truncating: 3 - 5 = 0. Source languages may use signed integers where 3 - 5 = -2.

Fix: Use Int when negative results are possible:

lean

def balance (deposits withdrawals : Int) : Int :=
  deposits - withdrawals  -- Can be negative

Show full SKILL.md (241 more words)Show less

5. Division by Zero

Problem: In Lean, division by zero returns zero (n / 0 = 0). Source languages may have preconditions preventing this.

Fix: Translate requires d != 0 as a hypothesis:

lean

def safeDivide (n d : Nat) (hd : d ≠ 0) : Nat := n / d

If callers are required to prove the divisor is nonzero, keep the hypothesis in the API type and translate the real body under that precondition.

6. Import Order

Problem: In Lean 4, import statements MUST be the very first non-comment content in a file. Module docstrings must come AFTER imports.

Symptom:

error: unexpected token 'namespace'; expected 'import'

Fix: Always structure files as:

lean

import ProjectName.Dependency

/-! Module docstring -/

namespace ProjectName.Module

7. autoImplicit Pitfalls

Problem: With autoImplicit = false (which we use), ALL type variables must be explicitly declared.

Symptom:

error: unknown identifier 'α'

Fix: Add explicit universe polymorphism:

lean

def push {α : Type} (s : Stack α) (v : α) : Stack α := ...
-- or use section variables:
variable {α : Type}

8. deriving Clause Limitations

Problem: Not all types can automatically derive all instances. Large structures (>10 fields) may fail to derive BEq or DecidableEq.

Fix: Skip BEq for large structures. Use manual instances only when the source semantics or tests actually require them:

lean

structure LargeConfig where
  field1 : Nat
  -- ... many fields
  deriving Inhabited, Repr  -- Skip BEq, DecidableEq

9. Mutual Recursion

Problem: Lean requires mutual ... end blocks for mutually recursive definitions, and termination must be proved for all functions in the block.

Fix:

lean

mutual
  def even : Nat → Bool
    | 0 => true
    | n + 1 => odd n
  def odd : Nat → Bool
    | 0 => false
    | n + 1 => even n
end

For curated benchmark sources, translate the real mutual bodies and add the needed termination hints. Pre-agent materialization introduces sorry later, after this source has already built.

10. Universe Polymorphism

Problem: Source languages don't have universe levels. In Lean, generic types may need explicit universe annotations.

Simple rule: Use Type (which is Type 0) unless you need higher universes. Most translations don't need universe polymorphism.

Files

Just SKILL.md in .claude/skills/vero-lean-pitfalls of sunblaze-ucb/vero.

Open the folder on GitHubat commit 0a7325d

Compare with similar skills

Vero Lean Pitfalls next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Vero Lean Pitfalls compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Vero Lean Pitfalls this skillsunblaze-ucb/vero	107	—	~1.4k	Automated safety check: Notes	Apache-2.0	1 mo ago
Translation Diff ExportDevolutions/UniGetUI	26k	—	~1.1k	Automated safety check: Pass	MIT	yesterday
Sync Translationssymfony/symfony	31k	—	~1.9k	Automated safety check: Pass	MIT	today
Translation Diff ImportDevolutions/UniGetUI	26k	—	~750	Automated safety check: Pass	MIT	yesterday
Translation Diff TranslateDevolutions/UniGetUI	26k	—	~934	Automated safety check: Pass	MIT	yesterday
Generate Translationspayloadcms/payload	45k	—	~1.1k	Automated safety check: Pass	MIT	yesterday

Similar skills

Translation Diff Export
Devolutions/UniGetUI
Compares UniGetUI JSON locale files against English, identifies untranslated or source-changed keys, and generates patch, reference, and handoff files for a target language.
26k GitHub stars~1.1k tokensUpdated yesterday
Writing & ContentAuto-check passed
Sync Translations
symfony/symfony
Synchronize translation catalogs across maintained Symfony branches: find messages that newer branches added to the English catalogs but that are still missing from the oldest maintained branch…
31k GitHub stars~1.9k tokensUpdated today
Writing & ContentAuto-check passed
Translation Diff Import
Devolutions/UniGetUI
Merges translated key-value pairs from a UniGetUI JSON localization patch back into the full language file and validates the merged result.
26k GitHub stars~750 tokensUpdated yesterday
Writing & ContentAuto-check passed
Translation Diff Translate
Devolutions/UniGetUI
Translates a sparse UniGetUI JSON language patch, writes completed entries into the working copy, preserves placeholders and terminology, and prepares the patch for merge-back.
26k GitHub stars~934 tokensUpdated yesterday
Writing & ContentAuto-check passed
Generate Translations
payloadcms/payload
A skill your agent uses when new translation keys are added to packages to generate new translations strings
45k GitHub stars~1.1k tokensUpdated yesterday
Writing & ContentAuto-check passed
InkOS Creative Harness
Narcooo/inkos
Drives long-form fiction, scripts, storyboards, interactive films and long-document translation through InkOS, with every change made by a typed action.
10k GitHub starsUsed in 1 repo~1.1k tokens
Writing & ContentAuto-check passed

Questions about Vero Lean Pitfalls

What does Vero Lean Pitfalls do?

Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation). Vero Lean Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation).

When should I use Vero Lean Pitfalls?

Vero Lean Pitfalls fits situations like: tasks that involve Translation.

How do I install Vero Lean Pitfalls in Claude Code?

Run `npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a claude-code`. Or copy the skill folder (.claude/skills/vero-lean-pitfalls in sunblaze-ucb/vero) into .claude/skills/vero-lean-pitfalls in your project. Claude Code loads it when a task matches its description.

How do I install Vero Lean Pitfalls in Codex?

Run `npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a codex`. Or copy the skill folder (.claude/skills/vero-lean-pitfalls in sunblaze-ucb/vero) into .agents/skills/vero-lean-pitfalls in your project. Codex loads it when a task matches its description.

Can I use Vero Lean Pitfalls in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add sunblaze-ucb/vero --skill vero-lean-pitfalls -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/vero-lean-pitfalls, .gemini/skills/vero-lean-pitfalls, .github/skills/vero-lean-pitfalls and .opencode/skills/vero-lean-pitfalls in your project.

What does Vero Lean Pitfalls need to run?

SKILL.md names no scripts, command-line tools or credentials: Vero Lean Pitfalls is instructions for the agent only. Its frontmatter pre-approves these tools: Read, Write, Edit, Bash, Grep, Glob.

Does Vero Lean Pitfalls access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Vero Lean Pitfalls safe to install?

Our automated static check of SKILL.md found notes only (pre-approves every shell command (allowed-tools: bash)), nothing it rates as a warning. It is not a guarantee. Review the folder before installing.

What licence does Vero Lean Pitfalls use?

Vero Lean Pitfalls is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Vero Lean Pitfalls use?

About 1.4k tokens (SKILL.md is roughly 5.5k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full.

What are the alternatives to Vero Lean Pitfalls?

Skills that share tags, products or a category with Vero Lean Pitfalls: Translation Diff Export (Devolutions/UniGetUI, 26k stars), Sync Translations (symfony/symfony, 31k stars), Translation Diff Import (Devolutions/UniGetUI, 26k stars) and Translation Diff Translate (Devolutions/UniGetUI, 26k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Vero Lean Pitfalls?

sunblaze-ucb (a GitHub organization) maintains it in sunblaze-ucb/vero, which has 107 GitHub stars. The repository holds 16 skills in this directory. The repository was last updated on August 17, 2026.

Source: sunblaze-ucb/vero on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.

Install Vero Lean Pitfalls

Facts

At a glance

What it does

When your agent uses it

Example prompts

Requirements

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

Lean 4 Translation Pitfalls

1. noncomputable Propagation

2. Standard Library Mappings

3. Prop vs Bool Confusion

4. Natural Number Subtraction

5. Division by Zero

6. Import Order

7. autoImplicit Pitfalls

8. deriving Clause Limitations

9. Mutual Recursion

10. Universe Polymorphism

Files

Compare with similar skills

Similar skills

More from sunblaze-ucb/vero

Related

Questions about Vero Lean Pitfalls