在Isabelle/HOL中有一个写为'a + 'b的sum-type，它允许您将两种不同类型的元素组合成一个新的类型. sum类型的两个构造函数是

There is the sum-type, written 'a + 'b, in Isabelle/HOL that allows you to combine elements of two different types into a new one. The two constructors of the sum type are

Inl :: 'a => 'a + 'b

用于向左注入和

Inr :: 'b => 'a + 'b

右插入.使用sum-type，您可以例如将数字nat list与纯数字nat的列表组合以获得(nat list) + nat.由于列表提供功能length :: 'a list => nat，因此您仍然可以在您知道它们是列表的不相加和元素上使用此功能.为了获取此信息(即，您查看的元素是列表还是纯数字)，我们通常使用 pattern-matching .

for inject right. Using the sum-type you could for example combine lists of numbers nat list with plain numbers nat to obtain (nat list) + nat. Since lists provide a function length :: 'a list => nat, you can still use this function on elements of the disjoint sum for which you know that they are lists. In order to obtain this information (i.e., whether the element you look at is a list or a plain number) we typically use pattern-matching.

如果当前元素是列表，则以下函数将计算列表的长度，否则仅返回其表示的数字.

The following function would compute the length of the list if the current element is a list and just return the number it represents, otherwise.

fun maybe_length :: "(nat list) + nat => nat"
where
  "maybe_length (Inl xs) = length xs" |
  "maybe_length (Inr n) = n"