Aliases serve as shorthand for terms, functions, and types, enhancing readability. Introduced through the declaration,
syntax alias <originalName> := <AlternativeName>;
these new names are interchangeable with the aliased name, applicable in pattern matching, qualification, and module opening.
Application of Aliases¶
Aliases can be forward referenced, permitting their use prior to declaration.
For instance, we define the alias Boolean for the
Bool type, and their terms
syntax alias Boolean := Bool; syntax alias ⊥ := false; syntax alias ⊤ := true; type Bool := | false | true; not : Boolean -> Boolean | ⊥ := ⊤ | ⊤ := ⊥;
Aliases exhibit versatility in application. They can be used in local definitions, as shown in the
let expression below.
localAlias : Binary -> Binary | b := let syntax alias b' := b; in b';
Like any other name, aliases can be exported from a module.
module ExportAlias; syntax alias Binary := Bool; syntax alias one := ⊤; syntax alias zero := ⊥; end; open ExportAlias; syntax operator || logical; || : Binary -> Binary -> Binary | zero b := b | one _ := one;
We can create aliases for not only types but also terms, including functions. For example, the binary
|| function can be aliased as
syntax alias or := ||; or3 (a b c : Binary) : Binary := or (or a b) c;