Datos de origen
- Repositorio
- benbrastmckie/ModelChecker
- Última actividad en el origen
- 4 de marzo de 2026 a las 00:47
- Idioma detectado de SKILL.md
- inglés
- Estrellas
- 13
- Forks
- 3
Opciones de instalación
De forma predeterminada está seleccionado el prompt que primero revisa el origen. Puedes cambiar a un comando directo o descargar una copia local.
Revisa los archivos de origen
Lee SKILL.md y los archivos complementarios que muestra SkillsMP antes de decidir si quieres instalarlo.
Mostrando SKILL.md
SKILL.md
Instrucciones de origen · Vista previa de solo lectura- name
- skill-lean-implementation
- description
- Implementation skill for Lean 4 proofs and definitions
- allowed_tools
- Read, Write, Edit, Bash, Grep, Glob, mcp__lean-lsp__*
- context
- project/lean4
# Lean Implementation Skill
Routes Lean 4 implementation tasks to lean-implementation-agent.
## Usage
Invoked by orchestrator when task language is `lean4` and operation is implementation.
## Agent
- **Agent**: lean-implementation-agent
- **Model**: default
## Context
- Lean 4 tactic patterns
- Proof structure templates
- MCP tools for proof assistance
Ver en GitHub