Agent Plugins Marketplace
← All plugins

write-lean-tests

v1.0.3

Conventions for compile-time, example-based Lean 4 API regression tests that mirror a library's public surface.

Claude Code1 Skill

By Christopher BooneLicense: MIT2 GitHub starsUpdated last week

Directory evidence

Runtimes
Claude Code
Parsed components
1 skill or MCP entry
Source updated
Sep 16, 2026
Manifest status
Canonical path parsed

The directory validates manifest shape and source location. It does not execute the plugin or provide a security endorsement. Review the indexing methodology →

Install write-lean-tests for Claude Code

Installs for the current user
claude plugin marketplace add IchenDEV/agent-plugin-mkt
claude plugin marketplace update agent-plugin-marketplace
claude plugin install write-lean-tests-2@agent-plugin-marketplace

Paste and run these commands in a terminal with Claude Code. They add and refresh the PluginsMP catalog, then install this plugin.

The installer fetches third-party code from the source repository shown on this page. This directory validates manifest structure and source location, but does not perform a security audit; review the manifest, components, and source before installing.

Get the source manually
git clone https://github.com/cboone/agent-harness-plugins

Clone the source repository, then follow its setup instructions to add the plugin to a compatible client. The plugin root is plugins/write-lean-tests/.

Plugin files

plugins/write-lean-tests/
├── .claude-plugin/plugin.json
└── skills/write-lean-tests/SKILL.md

Included Skills1

write-lean-testsskills/write-lean-tests/SKILL.md

Conventions for compile-time, `example`-based Lean 4 API regression tests that mirror a library's public surface. Use whenever Lean test code is the subject of the work, not only when editing: (1) creating, editing, or reviewing files under a `<Name>Test/` directory (sibling to the main `<Name>/` library directory), (2) adding a library module and deciding what its sibling test module should assert, (3) planning a milestone and scoping which `example`s must land alongside new exported definitions and lemmas, (4) diagnosing a failing or overly coupled test module (imports reaching into internals, `sorry` in test proofs, restating implementation rather than signature), (5) wiring `lake test` via `testDriver` / `defaultTargets` in a Lake config, (6) reviewing a PR that touches library or test code to check the test-mirroring invariant still holds. Pairs with `write-lean-code`, which owns naming, proof style, and Mathlib conventions for the library code itself.

Plugin manifests1

plugins/write-lean-tests/.claude-plugin/plugin.json
{
  "author": {
    "name": "Christopher Boone"
  },
  "description": "Conventions for compile-time, example-based Lean 4 API regression tests that mirror a library's public surface.",
  "homepage": "https://github.com/cboone/agent-harness-plugins",
  "keywords": [
    "formal-methods",
    "lean",
    "lean4",
    "mathlib",
    "testing"
  ],
  "license": "MIT",
  "name": "write-lean-tests",
  "repository": "https://github.com/cboone/agent-harness-plugins",
  "skills": "./skills",
  "version": "1.0.3"
}

For maintainers

If you maintain this plugin, link to this source-backed listing from your README so users can review its manifest and indexed components.

[write-lean-tests on Agent Plugins Marketplace](https://pluginsmp.com/plugins/write-lean-tests-2)