Skip to content

Refactor TreeMap to use simp_to_model #127

Open
Open
Refactor TreeMap to use simp_to_model#127
Labels
experimentIdeas for features that may or may not workgood first issueGood for newcomers
@markusdemedeiros

Description

@markusdemedeiros
markusdemedeiros
opened on Jan 22, 2026

The standard library has a tactic simp_to_model for proving facts about TreeMaps. We prove some facts about TreeMaps in HeapInstances.lean, but we do not make use of this automation yet. To make these proofs more robust, we should figure out how.

Metadata

Metadata

Assignees

No one assigned

    Labels

    experimentIdeas for features that may or may not workgood first issueGood for newcomers

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions