Structures

Structure is a special case of inductive datatype. It has only one constructor and is not recursive. Similar to the inductive command, the structure command introduces a namespace with the same name. The general form is as follows:

structure <name> <parameters> <parent-structures> where
  <constructor-name> :: <fields>

Most parts are optional. Here is our first example.

structure Point (α : Type u) where
  x : α
  y : α

In the example above, the constructor name is not provided. So, the constructor is named mk by Lean. Values of type Point are created using Point.mk a b or { x := a, y := b : Point α }. The latter can be written as { x := a, y := b } when the expected type is known. The fields of a point p are accessed using Point.x p and Point.y p. You can also the more compact notation p.x and p.y as a shorthand for Point.x p and Point.y p.

structure Point (α : Type u) where
 x : α
 y : α
#check Point
#check Point       -- Type u -> Type u
#check @Point.mk   -- {α : Type u} → α → α → Point α
#check @Point.x    -- {α : Type u} → Point α → α
#check @Point.y    -- {α : Type u} → Point α → α

#check Point.mk 10 20                   -- Point Nat
#check { x := 10, y := 20 : Point Nat } -- Point Nat

def mkPoint (a : Nat) : Point Nat :=
  { x := a, y := a }

#eval (Point.mk 10 20).x                   -- 10
#eval (Point.mk 10 20).y                   -- 20
#eval { x := 10, y := 20 : Point Nat }.x   -- 10
#eval { x := 10, y := 20 : Point Nat }.y   -- 20

def addXY (p : Point Nat) : Nat :=
  p.x + p.y

#eval addXY { x := 10, y := 20 }    -- 30

In the notation { ... }, if the fields are in different lines, the , is optional.

structure Point (α : Type u) where
 x : α
 y : α
def mkPoint (a : Nat) : Point Nat := {
  x := a
  y := a
}

You can also use where instead of := { ... }.

structure Point (α : Type u) where
 x : α
 y : α
def mkPoint (a : Nat) : Point Nat where
  x := a
  y := a

Here are some simple theorems about our Point type.

structure Point (α : Type u) where
 x : α
 y : α
theorem ex1 (a b : α) : (Point.mk a b).x = a :=
  rfl

theorem ex2 (a b : α) : (Point.mk a b).y = b :=
  rfl

theorem ex3 (a b : α) : Point.mk a b = { x := a, y := b } :=
  rfl

The dot notation is convenient not just for accessing the projections of a structure, but also for applying functions defined in a namespace with the same name. If p has type Point, the expression p.foo is interpreted as Point.foo p, assuming that the first argument to foo has type Point. The expression p.add q is therefore shorthand for Point.add p q in the example below.

structure Point (α : Type u) where
  x : α
  y : α

def Point.add (p q : Point Nat) : Point Nat :=
  { x := p.x + q.x, y := p.y + q.y }

def p : Point Nat := Point.mk 1 2
def q : Point Nat := Point.mk 3 4

#eval (p.add q).x  -- 4
#eval (p.add q).y  -- 6

After we introduce type classes, we show how to define a function like add so that it works generically for elements of Point α rather than just Point Nat, assuming α has an associated addition operation.

More generally, given an expression p.foo x y z, Lean will insert p at the first argument to foo of type Point. For example, with the definition of scalar multiplication below, p.smul 3 is interpreted as Point.smul 3 p.

structure Point (α : Type u) where
  x : α
  y : α

def Point.smul (n : Nat) (p : Point Nat) :=
  Point.mk (n * p.x) (n * p.y)

def p : Point Nat :=
  Point.mk 1 2

#eval (p.smul 3).x -- 3
#eval (p.smul 3).y -- 6

Inheritance

We can extend existing structures by adding new fields. This feature allows us to simulate a form of inheritance.

structure Point (α : Type u) where
  x : α
  y : α

inductive Color where
  | red
  | green
  | blue

structure ColorPoint (α : Type u) extends Point α where
  color : Color

#check { x := 10, y := 20, color := Color.red : ColorPoint Nat }
-- { toPoint := { x := 10, y := 20 }, color := Color.red }

The output for the check command above suggests how Lean encoded inheritance and multiple inheritance. Lean uses fields to each parent structure.

structure Foo where
  x : Nat
  y : Nat

structure Boo where
  w : Nat
  z : Nat

structure Bla extends Foo, Boo where
  bit : Bool

#check Bla.mk -- Foo → Boo → Bool → Bla
#check Bla.mk { x := 10, y := 20 } { w := 30, z := 40 } true
#check { x := 10, y := 20, w := 30, z := 40, bit := true : Bla }
#check { toFoo := { x := 10, y := 20 },
         toBoo := { w := 30, z := 40 },
         bit := true : Bla }

theorem ex :
    Bla.mk { x := x, y := y } { w := w, z := z } b
    =
    { x := x, y := y, w := w, z := z, bit := b } :=
  rfl

Default field values

You can assign default value to fields when declaring a new structure.

inductive MessageSeverity
  | error | warning

structure Message where
  fileName : String
  pos      : Option Nat      := none
  severity : MessageSeverity := MessageSeverity.error
  caption  : String          := ""
  data     : String

def msg1 : Message :=
  { fileName := "foo.lean", data := "failed to import file" }

#eval msg1.pos      -- none
#eval msg1.fileName -- "foo.lean"
#eval msg1.caption  -- ""

When extending a structure, you can not only add new fields, but provide new default values for existing fields.

inductive MessageSeverity
 | error | warning
structure Message where
 fileName : String
 pos      : Option Nat      := none
 severity : MessageSeverity := MessageSeverity.error
 caption  : String          := ""
 data     : String
structure MessageExt extends Message where
  timestamp : Nat
  caption   := "extended" -- new default value for field `caption`

def msg2 : MessageExt where
  fileName  := "bar.lean"
  data      := "error at initialization"
  timestamp := 10

#eval msg2.fileName  -- "bar.lean"
#eval msg2.timestamp -- 10
#eval msg2.caption   -- "extended"

Updating structure fields

Structure fields can be updated using { <struct-val> with <field> := <new-value>, ... }:

structure Point (α : Type u) where
 x : α
 y : α
def incrementX (p : Point Nat) : Point Nat := { p with x := p.x + 1 }