Naming Conventions

  • Sessions in the AFP and community projects are named in capitalized Snake_Case, e.g. Akra_Bazzi. We follow this convention.
    • Note that in the distribution session are named with capitalized words separated by hyphens, e.g. HOL-Analysis, HOL-Library.
  • Theory names: capitalized Snake_Case, e.g. Sepref_All_Examples.

  • If theories and sessions are named in this way, imports never need to need quotation marks, i.e. one can write Akra_Bazzi.Akra_Bazzi instead of "Akra_Bazzi". Thus the latter form should never be used.

Session Discipline

  • One session per project is the norm.

Folders and Theory Naming

Projects should be hierarchically structured using folders. Each project must come with a and LICENSE file. Theory names are generally captilised with underscores. The theory name must describe the main content of the theory. Example

│   │   Monoids.thy
│   │   Groups.thy
│   │   ...
│   └───Continued_Fractions
│       │   Continued_Fractions_Basics.thy
│       │   Continued_Fractions_Recurrence.thy
│       │   Continued_Fractions_Limits.thy
│       │   ...
    │   ...