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
versustc_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