Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 12
    • Merge requests 12
  • 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
  • stdpp
  • Merge requests
  • !168

add singleton_insert_empty

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Ralf Jung requested to merge ralf/singleton_insert_empty into master Jun 29, 2020
  • Overview 9
  • Commits 1
  • Pipelines 0
  • Changes 1

This is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/singleton_insert_empty