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 10
    • Merge requests 10
  • 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
  • !436

lookup_gset_to_gmap: use decide rather than guard

  • Review changes

  • Download
  • Email patches
  • Plain diff
Closed Ralf Jung requested to merge ralf/lookup_gset_to_gmap into master Dec 15, 2022
  • Overview 8
  • Commits 1
  • Pipelines 1
  • Changes 1

guard is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. decide is a lot more common, and so people are more likely to know how to deal with it.

Edited Dec 15, 2022 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: ralf/lookup_gset_to_gmap