Notation for Option?

Stream: lean4

[Paul Chisholm]

When using Lean as a programming language the Option type will be used quite extensively and can contribute to large type expressions. Could consideration be given to introducing standard abbreviated notation for Option. As a test I added

notation "⟦" a "⟧" => Option a

and found the resulting code to be cleaner with less syntactic baggage. (Note: not proposing this as a notation, just to demonstrate.)