Skip to content

GitLab

I
Iris
Open
Opened 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 by Ralf Jung