When to use and when not to use parenthesis?

Stream: new members

[Youngju Song]

I found that variable keyword enforces parenthesis whereas axiom keyword enforces "not" to use parenthesis:

variable (a: Nat)
variable a: Nat -- does not type check
axiom (a: Nat) -- does not type check
axiom a: Nat

This looks like an intentional design, but I am not catching the intent.

[Eric Wieser]

axiom should be compared to def, not to variable

[Niels Voss]

This is because variable is intended to mimick the syntax of an individual parameter in a def, while axiom is intended to mimick the syntax of a def itself. So, in

def f (n : Nat) : Nat := sorry

the variable command uses the syntax of (n : Nat) while axiom uses the syntax of f ... : Nat.

Another way to see this is that it makes sense to have a variable become an implicit parameter like variable {a : Nat} or typeclass inferred parameter like variable [inst : Nonempty T], but it would not make sense to have something like axiom {c : Nat} because c is the identifier name.

[Youngju Song]

@Eric Wieser @Niels Voss Thank you for the explanation! That makes very much sense, and I like the design!

[Kyle Miller]

Terminology note: axiom (a: Nat) doesn't parse. If you see "unexpected token", then it neither type checks nor doesn't type check, because it is not syntactically meaningful.

[Youngju Song]

@Kyle Miller Right, thanks for pointing this out!