rocq-stdpp
Facts about stdpp maps, sets, finite sets, lookup, insertion, deletion, domains, and set automation.
Skill by jialunzhang-psu
Chalk Labs
Need help deploying rocq-stdpp?
Chalk Labs sets up agents like this inside real teams: connected to your tools, tested on your data, with a human in the loop where it matters.
Install
Works with Claude Code, Claude apps, Codex, Cursor, Gemini CLI, GitHub Copilot, VS Code, OpenCode, Goose, Windsurf. Read the repository before you give any tool access to your data.
npx agentmarket install skill/jialunzhang-psu-rocq-stdpp
Asks which of your tools to add it to (Claude Code, Codex, Cursor, VS Code, Windsurf, Gemini CLI, Claude Desktop) and shows the change first. See https://agentmart.dev/cli.
Get the weekly diff
The weekly diff: one email a week with new agent tools, notable updates and grade changes, plus security alerts for tools you follow. Double opt-in, one-click unsubscribe.
About
Reviews
Write a reviewNo reviews yet. Installed it? Reviews come from verified installers only. How reviews work
Permissions
What this skill can do and what it asks for, from its SKILL.md. Checked Oct 25, 2026.
- Tools
- No tools found
- Secrets
- None asked for
- Install scripts
- None found
Network hosts it talks to 1
codeload.github.com· found in install command
Files it touches
~/.claude/skills/rocq-stdpp
What's inside
- Skill name
rocq-stdpp- Description
- Facts about stdpp maps, sets, finite sets, lookup, insertion, deletion, domains, and set automation.
- License
- Apache-2.0
- Instructions
- 26 lines in SKILL.md · view on GitHub
Files (3)
- SKILL.md
- maps.md · references/
- sets.md · references/
SKILL.md (first lines)
# stdpp Map and Set Facts - `m !! k` denotes a stdpp map lookup. - `<[k:=v]> m` denotes insertion or replacement at key `k`. - `delete k m` denotes deletion of `k` from a map. - `dom m` denotes the domain of a map. - `map_eq` changes map equality into equality of lookups at each key when applied to a map equality goal. - `lookup_insert_eq` describes lookup at the inserted key. - `lookup_insert_ne` describes lookup at a key different from the inserted key. - `lookup_delete_eq` and `lookup_delete_ne` describe lookup after deletion. - `lookup_insert_Some` decomposes a successful lookup in an inserted map. - `elem_of_dom_2` connects a successful lookup with domain membership. - `not_elem_of_dom` connects absence from a domain with lookup failure. - `set_unfold` exposes set membership expressions. - `set_solver` solves supported pure set-algebra goals. ```coq apply map_eq; intro k. rewrite lookup_insert_eq. rewrite lookup_insert_ne by congruence. rewrite lookup_delete_eq. rewrite lookup_delete_ne by congruence. ```
From jialunzhang-psu/rocq-mcp, Apache-2.0.
More from jialunzhang-psu/rocq-mcp
- 0.567score
rocq-stdlib-lemmas
jialunzhang-psu
Facts about Rocq Stdlib modules for arithmetic, booleans, options, lists, strings, relations, permutations, and equality.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-spec-review
jialunzhang-psu
Facts about Rocq declaration surfaces, assumptions reports, proof-free documentation views, and source-level specification extraction.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-induction-generalization
jialunzhang-psu
Facts about Rocq induction principles, variable generalization, strong induction, dependent induction, and statement strengthening.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-inversion-discrimination
jialunzhang-psu
Facts about constructor disjointness, constructor injectivity, inversion, discrimination, and case analysis for Rocq inductive types.
SkillAFreshness: AClaude Code +9 - 0.564score
rocq-typeclasses
jialunzhang-psu
Facts about Rocq typeclass and canonical-instance resolution, setoid rewriting, and instance debugging.
SkillAFreshness: AClaude Code +9 - 0.564score
rocq-dependent-rewriting
jialunzhang-psu
Facts about equality rewriting, transport, and elimination in dependent and indexed Rocq/Coq types.
SkillAFreshness: AClaude Code +9 - 0.564score
rocq-subgoal-focusing
jialunzhang-psu
Facts about Rocq goal focus, bullets, braces, and multiple-goal diagnostics.
SkillAFreshness: AClaude Code +9 - 0.561score
rocq-recursion-termination
jialunzhang-psu
Facts about Rocq structural recursion, guard checking, well-founded recursion, fuel parameters, and coinductive productivity.
SkillAFreshness: AClaude Code +9 - 0.558score
rocq-compile-error-triage
jialunzhang-psu
Facts about Rocq parser, kernel, tactic, universe, name-resolution, termination, and proof-closing diagnostics.
SkillAFreshness: AClaude Code +9 - 0.558score
rocq-dune-loadpath
jialunzhang-psu
Facts about Dune Rocq theories, logical load paths, project files, and physical-to-logical module mappings.
SkillAFreshness: AClaude Code +9 - 0.558score
rocq-axiom-audit
jialunzhang-psu
Facts about Rocq assumptions, axioms, admitted declarations, and trust inspection.
SkillAFreshness: AClaude Code +9 - 0.553score
rocq-library-search
jialunzhang-psu
Facts about Rocq declaration search and inspection commands, local contexts, and the connected MCP query forms.
SkillAFreshness: AClaude Code +9
Signals
- Stars
- 0
- Forks
- 0
- Open issues
- 0
- Last commit (this folder)
- Sep 28, 2026 (1 month ago)
From GitHub (fetched Oct 24, 2026).
Details
- License
- Apache-2.0
- Repository
- github.com/jialunzhang-psu/rocq-mcp
- First seen
- Oct 24, 2026
- Last checked
- Oct 24, 2026
- Source
- GitHubgithub-graphql
More from jialunzhang-psu
- 0.567score
rocq-spec-review
jialunzhang-psu
Facts about Rocq declaration surfaces, assumptions reports, proof-free documentation views, and source-level specification extraction.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-induction-generalization
jialunzhang-psu
Facts about Rocq induction principles, variable generalization, strong induction, dependent induction, and statement strengthening.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-inversion-discrimination
jialunzhang-psu
Facts about constructor disjointness, constructor injectivity, inversion, discrimination, and case analysis for Rocq inductive types.
SkillAFreshness: AClaude Code +9 - 0.567score
rocq-stdlib-lemmas
jialunzhang-psu
Facts about Rocq Stdlib modules for arithmetic, booleans, options, lists, strings, relations, permutations, and equality.
SkillAFreshness: AClaude Code +9 - 0.564score
rocq-subgoal-focusing
jialunzhang-psu
Facts about Rocq goal focus, bullets, braces, and multiple-goal diagnostics.
SkillAFreshness: AClaude Code +9 - 0.564score
rocq-typeclasses
jialunzhang-psu
Facts about Rocq typeclass and canonical-instance resolution, setoid rewriting, and instance debugging.
SkillAFreshness: AClaude Code +9
Done for you
Rather not set it up yourself?
Chalk Labs scopes, builds and runs agents for your team: the task audit, the eval harness, the integrations and the weekly ops report. Fixed scope, priced before we start.
See how we build AI agents →Read the case studies
Chalk Labs is a two-founder AI and growth studio. We build AI agents, CRMs and MVPs for Web3 and AI companies, and have shipped 50+ product and token launches.
- launches shipped
- 50+
- launches shipped
- media placements
- 500+
- media placements
- founders on every account
- 2
- founders on every account
Press we've placed: Forbes · CoinDesk · Decrypt · Cointelegraph · The Block
Rahil Jain, Co-founder, Chalk Labs. Ex-Goldman Sachs engineer. You talk to the person who builds it.
Get rocq-stdpp running in your business
Tell us what you want to automate. A founder replies within one working day with a plan, not a pitch deck.
Cite this page
rocq-stdpp skill. Agent Mart. https://agentmart.dev/skills/jialunzhang-psu-rocq-stdpp (last updated 2026-10-24)