Skip to content

GitLab

I
Iris
Open
Opened by Robbert@robbertkrebbers
Report abuse New issue

Create example user library

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 by Ralf Jung

The one place for your designs

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.