Formatting axioms

[janmasrovira]

• As part of Fix: pprint positive kw for data types #1980, the formatting of the axiom keyword has changed. Here I intend to start a discussion on what formatting would make more sense.

We are considering two options:
Option A.

axiom 
boom : {A : Type} -> A;

Option B.

axiom boom : {A : Type} -> A;

Note that regardless of the option that we chose for the formatter, both options will still be acceptable by the parser.

The strong points that I have gathered for each option include:

Option A.

1. Easy to comment out.
2. Consistency with the positive and terminating keywords.

Option B.

1. It seems to be a convention to have the keyword (axiom or equivalent) next to the name in other languages. All Agda, Coq, Idris and Lean write the keyword just before the name. I personally think that this is a reasonable and intuitive convention.

[lukaszcz]

I'm in favour of option B, because logically axiom belongs to a different category than positive or terminating. It indicates the kind of thing you are defining, like fun (if we had it), macro, type, etc. The positive and terminating are annotations specifying some attributes of your definition, not what kind of definition this is. It's a fairly common convention to specify the kind of definition on the same line. It's rather rare that you want to change one kind of definition into another kind, while adding and removing attributes is more common.

Hence, I think point 1 for option A is weak. Point 2 is actually a counter-point, because you're trying to keep consistency with things that are in a different category, arguably risking confusion between those two categories (attributes and definition kind specifiers).