Sum, a small algebra of choices

By Jonathan Prieto-CubidesPublished Aug 3, 2026

Defining `Sum`

The constructors

This post introduces a tiny sum type. The companion post on using Sum uses the definition in a different piece of writing, while the PostSource reference demonstrates a link from English prose to a generated Lean declaration.

inductive Sum (α β : Type) where
  | left : α → Sum α β
  | right : β → Sum α β

Visualizing the choice

The value is always on exactly one side:

flowchart LR Value --> Left[Sum.left] Value --> Right[Sum.right]

See raw

Defining Sum

The constructors

Visualizing the choice

Continue reading

Using Sum in another post

A LeanBlog post

How a LeanBlog post is built

Defining `Sum`