Skip to content

Port iInduction #360

Open
Open
Port iInduction#360
Labels
featNew feature or requestportingPorting Rocq developmentproof-modeProofMode porting tasks
@MackieLoeffel

Description

@MackieLoeffel
MackieLoeffel
opened on Apr 24, 2026

See Iris Rocq documentation at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md

Metadata

Metadata

Assignees

No one assigned

    Labels

    featNew feature or requestportingPorting Rocq developmentproof-modeProofMode porting tasks

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions