Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Issues
  • #276

Closed
Open
Opened Dec 02, 2019 by Robbert Krebbers@robbertkrebbersMaintainer

Create example user library and document library best practices

During a discussion at MPI with @jung @haidang @lepigre @msammler, we figured it may be a good idea to make a sample file to demonstrate the various conventions in Iris.

Possible aspects the file could cover:

  • Section structure, definitions outside of sections
  • Sealing
  • Params
  • Typeclasses Opaque versus tc_opaque
  • inG and Σs
  • Implicit Types
  • Indenting, use of bullets, use of braces
  • Styles of WP and Texan Triple lemmas, e.g. use of binders, value pairs
Edited Aug 06, 2020 by Ralf Jung
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#276