Plugin Claude Code
math-comp / mathcomp-analysis Rocq style guide, validated cleanup patterns, a read-only review command, and a per-file style auditor subagent — rocq-mcp-aware.
5 27d ago A
tokens not measured
original Apache-2.0
Agent
Read-only per-file mathcomp / mathcomp-analysis style auditor. Dispatch one instance PER FILE to produce a structured punch list of style violations keyed to reference.md section numbers. Use when /mathcomp-review fans out, or whenever a thorough style audit of one or more .v files is wanted. Never edits files.
5 27d ago A 70 tokens
original Apache-2.0
Command
Read-only mathcomp / mathcomp-analysis style review of .v files.
5 27d ago A 18 tokens
original Apache-2.0
PostToolUse
04Hook
Runs after a tool call finishes for Edit and Write tool calls, executing run-audit.sh. From LLM4Rocq/mathcomp-skills.
5 27d ago A
tokens not measured
original Apache-2.0
Skill Claude CodeCodex
Use when writing or reviewing .v files that import From mathcomp or From HB — math-comp, mathcomp-analysis, Rocq style, ssreflect tactics, HB hierarchy builder, HB factory, forgetful inheritance, canonical structures, Arguments directives, lemma naming (mainSymbolsuffixes, abbreviation suffixes), intro patterns…
5 27d ago A 149 tokens
original Apache-2.0