Agent skill

Vero Coq Pitfalls

Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls.

Apache-2.0Auto-check: notesWriting & Content

Install Vero Coq Pitfalls

skills CLI

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

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

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-coq-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-coq-pitfalls .claude/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .claude/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-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-coq-pitfalls -a codex

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

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-coq-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-coq-pitfalls .agents/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .agents/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-pitfalls -a cursor

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

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-coq-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-coq-pitfalls .cursor/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .cursor/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-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-coq-pitfalls -a gemini-cli

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

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-coq-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-coq-pitfalls .gemini/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .gemini/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-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-coq-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-coq-pitfalls .github/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .github/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-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-coq-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-coq-pitfalls .opencode/skills/vero-coq-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-coq-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-coq-pitfalls into .opencode/skills/vero-coq-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-coq-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-coq-pitfalls
GitHub stars: 107
Token cost: ~1.5k tokens
SKILL.md length: 481 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 translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls.

Works in 10 steps: Fixpoint → def with termination_by → Inductive / Record → inductive / structure → Prop / Set / Type Universe Mapping → …
Tasks that involve Translation
SKILL.md covers 1. Fixpoint → def with…, 2. Inductive / Record →…, 3. Prop / Set / Type Universe… and 4. Section Variables, plus 6 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Vero Coq Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls. Pair with vero-source-coq and vero-lean-pitfalls.

Its SKILL.md is about 1.5k 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-coq-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.

Fixpoint → def with termination_by
Inductive / Record → inductive / structure
Prop / Set / Type Universe Mapping
Section Variables
Coq Tactics → Lean Tactics
Program / Program Fixpoint
Module System
Notation and Coercions
Dependent Types
Extraction vs Compilation

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 coq).
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 Coq Pitfalls loads about 1.5k tokens when it runs. Until then it costs about 37 tokens; SKILL.md has 481 words of instructions outside code blocks.

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

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). 481 words, ~1,507 tokens.

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

name: vero-coq-pitfalls
description: Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls. Pair with vero-source-coq and vero-lean-pitfalls.
allowed-tools: Read, Write, Edit, Bash, Grep, Glob

Coq → Lean 4 Translation Pitfalls

Issues specific to translating Coq to Lean 4.

1. Fixpoint → def with termination_by

Coq:

coq

Fixpoint length {A : Type} (l : list A) : nat :=
  match l with
  | nil => 0
  | cons _ t => S (length t)
  end.

Lean:

lean

def length {α : Type} (l : List α) : Nat :=
  match l with
  | [] => 0
  | _ :: t => 1 + length t

Lean can often infer structural recursion automatically. Add termination_by only when needed:

lean

termination_by l.length

For curated API reference implementations, add termination_by when Lean cannot infer structural recursion. The LLM-facing sorry is introduced later by pre-agent materialization, not in the curated source.

2. Inductive / Record → inductive / structure

Coq:

coq

Inductive tree (A : Type) : Type :=
| Leaf : tree A
| Node : A -> tree A -> tree A -> tree A.

Record point := { x : Z; y : Z }.

Lean:

lean

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : α → Tree α → Tree α → Tree α
  deriving Inhabited, Repr

structure Point where
  x : Int
  y : Int
  deriving Inhabited, Repr

Key differences:

Coq constructors are top-level; Lean constructors are namespaced (Tree.leaf not just leaf)
Coq Record becomes Lean structure (with field projection)
Add deriving Inhabited when default values are actually needed by translated code/tests; do not add instances just because a downstream proof might want them.

3. Prop / Set / Type Universe Mapping

Coq	Lean	Notes
`Prop`	`Prop`	Direct correspondence
`Set`	`Type`	Coq `Set` ≈ Lean `Type 0`
`Type`	`Type 1`	Coq `Type` is one level higher than `Set`
`bool`	`Bool`	Computational booleans
`nat`	`Nat`	Natural numbers
`Z`	`Int`	Integers

Common mistake: Translating Coq Set as Lean Set — Lean's Set α is α → Prop (a predicate), NOT a universe level. Use Type instead.

4. Section Variables

Coq:

coq

Section MySection.
  Variable A : Type.
  Variable f : A -> A.

  Definition apply_twice (x : A) : A := f (f x).
End MySection.
(* apply_twice : forall A : Type, (A -> A) -> A -> A *)

Lean:

lean

-- Option 1: explicit parameters
def applyTwice {α : Type} (f : α → α) (x : α) : α := f (f x)

-- Option 2: section variables (closer to Coq style)
section MySection
  variable {α : Type}
  variable (f : α → α)

  def applyTwice (x : α) : α := f (f x)
end MySection

Key: Coq Variable in a Section becomes implicit after End. In Lean, use variable in a section for the same effect.

5. Coq Tactics → Lean Tactics

Coq tactic	Lean equivalent	Notes
`intro`	`intro`	Same
`apply`	`apply`	Same
`exact`	`exact`	Same
`rewrite`	`rw`	Lean uses `rw`
`simpl`	`simp`	Different behavior — Lean `simp` is more powerful
`unfold`	`unfold`	Same
`destruct`	`cases` or `match`
`induction`	`induction`	Same
`omega`	`omega`	Same (for linear arithmetic)
`ring`	`ring`	Same
`auto`	`simp` or `aesop`	No direct equivalent
`trivial`	`trivial`	Same
`reflexivity`	`rfl`	Lean uses `rfl`
`split`	`constructor` or `And.intro`
`left`/`right`	`left`/`right`	Same
`exists`	`use` or `exact ⟨...⟩`
`assert`	`have`
`pose`	`let`
`lia`	`omega`	Linear integer arithmetic

Curation rule: source proofs become benchmark specs, not curation-time Lean theorem proofs. Use this tactic mapping only when you are translating proof-relevant vocabulary or checking an auxiliary lemma by hand.

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

6. Program / Program Fixpoint

Problem: Coq Program allows partial definitions with obligations. In Lean, these become regular def with proof obligations as separate theorems.

Coq:

coq

Program Fixpoint merge (l1 l2 : list nat) {measure (length l1 + length l2)} :=
  ...

Lean:

lean

def merge (l1 l2 : List Nat) : List Nat :=
-- !benchmark @start code def=merge
  -- translated merge body
  ...
-- !benchmark @end code def=merge
termination_by l1.length + l2.length

7. Module System

Coq:

coq

Module Stack.
  Definition t := list nat.
  Definition push := cons.
End Stack.

Lean:

lean

namespace Stack
  def T := List Nat
  def push := List.cons
end Stack

Coq Module Type (interfaces) → Lean class or structure:

lean

class StackInterface (S : Type) where
  push : S → Nat → S
  pop : S → Option (Nat × S)

8. Notation and Coercions

Problem: Coq notations (`( ... )) and coercions don't transfer.

Fix: Replace Coq notations with explicit Lean function calls. If the notation is widely used, define a Lean notation or scoped notation:

lean

scoped notation "⟦" x "⟧" => interpret x

For API reference implementations, prefer explicit function calls unless the notation materially improves readability and is used consistently.

9. Dependent Types

Coq:

coq

Definition safe_head {A} (l : list A) (H : l <> nil) : A := ...

Lean:

lean

def safeHead {α : Type} (l : List α) (h : l ≠ []) : α :=
  match l with
  | [] => False.elim (h rfl)
  | x :: _ => x

The dependent proof parameter h : l ≠ [] transfers directly.

10. Extraction vs Compilation

Problem: Coq uses extraction (Extraction) to produce OCaml/Haskell. Lean compiles directly. Functions marked Extraction Inline or with Extract Constant have no Lean equivalent.

Fix:

Extract Constant f => "..." → opaque f ... (external boundary)
Extraction Inline f → just define f normally (Lean inlines via compiler)
If the extracted constant is a standard operation, map to Lean stdlib

Files

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

Open the folder on GitHubat commit 0a7325d

Compare with similar skills

Vero Coq 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 Coq Pitfalls compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Vero Coq Pitfalls this skillsunblaze-ucb/vero	107	—	~1.5k	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 Coq Pitfalls

What does Vero Coq Pitfalls do?

Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls. Vero Coq Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls.

When should I use Vero Coq Pitfalls?

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

How do I install Vero Coq Pitfalls in Claude Code?

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

How do I install Vero Coq Pitfalls in Codex?

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

Can I use Vero Coq 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-coq-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-coq-pitfalls, .gemini/skills/vero-coq-pitfalls, .github/skills/vero-coq-pitfalls and .opencode/skills/vero-coq-pitfalls in your project.

What does Vero Coq Pitfalls need to run?

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

Does Vero Coq 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 Coq 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 Coq Pitfalls use?

Vero Coq 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 Coq Pitfalls use?

About 1.5k tokens (SKILL.md is roughly 6k 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 Coq Pitfalls?

Skills that share tags, products or a category with Vero Coq 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 Coq 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 Coq 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

Coq → Lean 4 Translation Pitfalls

1. Fixpoint → def with termination_by

2. Inductive / Record → inductive / structure

3. Prop / Set / Type Universe Mapping

4. Section Variables

5. Coq Tactics → Lean Tactics

6. Program / Program Fixpoint

7. Module System

8. Notation and Coercions

9. Dependent Types

10. Extraction vs Compilation

Files

Compare with similar skills

Similar skills

More from sunblaze-ucb/vero

Related

Questions about Vero Coq Pitfalls