lean4-theorem-value-access
bydisentinel· 40 skills
Fix missing theorem proof terms when analyzing Lean 4 environments via importModules. Use when: (1) ConstantInfo.value? returns none for theorems despite TheoremVal.value being Expr, (2) building code graph / dependency extractor for Lean 4 and getting 0 proof dependency edges, (3) Lean 4.30+ project where theorem proofs appear missing from loaded environment, (4) analyzing Mathlib or any Lean 4 project and proof terms are empty. Root cause: breaking change in Lean 4.30 — value? treats theorems as opaque by default.
How to install lean4-theorem-value-access?
disentinel/grafema/lean4-theorem-value-access
$npx -y skills add disentinel/grafema --skill lean4-theorem-value-accessInstalls into the current project.
›Prefer a prompt? Paste this to your agent
Run `npx skills use "https://github.com/disentinel/grafema" --skill "disentinel/grafema/lean4-theorem-value-access"` and follow the generated skill instructions now. Read its complete output, redirecting it to a temporary file first if necessary. Resolve relative paths from the supporting-files directory it provides.
Use the skills in "https://github.com/disentinel/grafema" that are relevant to the current task. Run `npx skills add "https://github.com/disentinel/grafema"` and select the relevant skills, then follow their instructions.
Related
6 picksType
- improve-codebase-architectureScan a codebase for deepening opportunities, present them as a visual HTML report, then grill through whichever one you pick.Jul 2026
- domain-modelingBuild and sharpen a project's domain model. Use when the user wants to pin down domain terminology or a ubiquitous language, record an architectural decision,…Jul 2026
- caveman-reviewUltra-compressed code review comments. Cuts noise from PR feedback while preserving the actionable signal. Each comment is one line: location, problem, fix.Jul 2026
- codebase-designShared vocabulary for designing deep modules. Use when the user wants to design or improve a module's interface, find deepening opportunities, decide where a…Jul 2026
- code-reviewReview the changes since a fixed point (commit, branch, tag, or merge-base) along two axes — Standards (does the code follow this repo's documented coding…Jul 2026
- resolving-merge-conflictsUse when you need to resolve an in-progress git merge/rebase conflict.Jul 2026
