Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #429
Closed
Open
Issue created Jul 23, 2021 by Ralf Jung@jungOwner

Enable the use of the proofmode for proving big-op lemmas

There are many things that are painful about bi/big_op.v, but one of the biggest ones is the fact that we cannot use the proofmode to prove these lemmas -- because the proofmode actually uses big-ops itself.

It would be good to find some way to stratify this, so that only some core set of lemmas needs to be shown without the proofmode, and the rest can use the proofmode.

Assignee
Assign to
Time tracking