Aliases

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 true and false as ⊤ and ⊥ respectively.

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 or.

syntax alias or := ||;

or3 (a b c : Binary) : Binary := or (or a b) c;