Additional Conveniences

Shared Argument Types

When defining a function that takes multiple arguments that have the same type, both can be written before the same colon. For example,

def equal? [BEq α] (x : α) (y : α) : Option α :=
  if x == y then
    some x
  else
    none

can be written

def equal? [BEq α] (x y : α) : Option α :=
  if x == y then
    some x
  else
    none

This is especially useful when the type signature is large.

Leading Dot Notation

The constructors of an inductive type are in a namespace. This allows multiple related inductive types to use the same constructor names, but it can lead to programs becoming verbose. In contexts where the inductive type in question is known, the namespace can be omitted by preceding the constructor's name with a dot, and Lean uses the expected type to resolve the constructor names. For example, a function that mirrors a binary tree can be written:

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

Omitting the namespaces makes it significantly shorter, at the cost of making the program harder to read in contexts like code review tools that don't include the Lean compiler:

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

Using the expected type of an expression to disambiguate a namespace is also applicable to names other than constructors. If BinTree.empty is defined as an alternative way of creating BinTrees, then it can also be used with dot notation:

def BinTree.empty : BinTree α := .leaf

#check (.empty : BinTree Nat)

BinTree.empty : BinTree Nat

Or-Patterns

In contexts that allow multiple patterns, such as match-expressions, multiple patterns may share their result expressions. The datatype Weekday that represents days of the week:

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
  deriving Repr

Pattern matching can be used to check whether a day is a weekend:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

This can already be simplified by using constructor dot notation:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

Because both weekend patterns have the same result expression (true), they can be condensed into one:

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

This can be further simplified into a version in which the argument is not named:

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

Behind the scenes, the result expression is simply duplicated across each pattern. This means that patterns can bind variables, as in this example that removes the inl and inr constructors from a sum type in which both contain the same type of value:

def condense : α ⊕ α → α
  | .inl x | .inr x => x

Because the result expression is duplicated, the variables bound by the patterns are not required to have the same types. Overloaded functions that work for multiple types may be used to write a single result expression that works for patterns that bind variables of different types:

def stringy : Nat ⊕ Weekday → String
  | .inl x | .inr x => s!"It is {repr x}"

In practice, only variables shared in all patterns can be referred to in the result expression, because the result must make sense for each pattern. In getTheNat, only n can be accessed, and attempts to use either x or y lead to errors.

def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat
  | .inl (n, x) | .inr (n, y) => n

Attempting to access x in a similar definition causes an error because there is no x available in the second pattern:

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => x

unknown identifier 'x'

The fact that the result expression is essentially copy-pasted to each branch of the pattern match can lead to some surprising behavior. For example, the following definitions are acceptable because the inr version of the result expression refers to the global definition of str:

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

Calling this function on both constructors reveals the confusing behavior. In the first case, a type annotation is needed to tell Lean which type β should be:

#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))

"twenty"

In the second case, the global definition is used:

#eval getTheString (.inr (20, "twenty"))

"Some string"

Using or-patterns can vastly simplify some definitions and increase their clarity, as in Weekday.isWeekend. Because there is a potential for confusing behavior, it's a good idea to be careful when using them, especially when variables of multiple types or disjoint sets of variables are involved.