Skip to content

docs(lean4): add simp and simproc skill - #47

Open
alok wants to merge 2 commits into
cameronfreer:mainfrom
alok:codex/lean4-simp-simprocs-pr
Open

docs(lean4): add simp and simproc skill#47
alok wants to merge 2 commits into
cameronfreer:mainfrom
alok:codex/lean4-simp-simprocs-pr

Conversation

@alok

@alok alok commented Mar 13, 2026

Copy link
Copy Markdown
Contributor

Summary

  • add a focused lean4-simp-simprocs skill inside the unified lean4 plugin
  • expand the shared simp-hygiene and simproc-patterns references with decision rules and authoring guidance grounded in the Lean community simp/simproc blog posts
  • surface the new skill in the root and plugin READMEs so it is discoverable alongside the other focused Lean 4 skills

Verification

  • ran bash plugins/lean4/tools/lint_docs.sh --verbose
  • lint still reports existing broken anchors and metadata warnings elsewhere in the repo; this change did not introduce a new lint class

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant