Inductive Types

The main type construction in Lean is the inductive type. We will see how to define inductive types and how to define functions by recursion on these types.

We have already seen one special case of inductive types: structures. In ShortAnswer, we saw another special case, namely enumerated types. We will now see a third special case, namely non-recursive inductive types. Finally, we will see the general case, namely recursive inductive types.

inductive Answer : Type

The Answer type is a non-recursive inductive type, with constructors a short answer or a short answer with reason.

• just (ans : ShortAnswer) : Answer
• because (ans : ShortAnswer) (reason : String) : Answer

def Answer.eg₁ : Answer

An example of a term in the Answer type.

Equations

• Answer.eg₁ = Answer.because ShortAnswer.yes "I said so"

def Answer.short (a : Answer) : ShortAnswer

The short answer to an answer.

Equations

• (Answer.just ans).short = ans
• (Answer.because ans reason).short = ans

The dot notation.

inductive LongAnswer : Type

A LongAnswer is either a ShortAnswer or a LongAnswer with a reason.

• just (ans : ShortAnswer) : LongAnswer
• because (ans : LongAnswer) (reason : String) : LongAnswer

def LongAnswer.eg₁ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₁ = LongAnswer.just ShortAnswer.yes

def LongAnswer.eg₂ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₂ = (LongAnswer.just ShortAnswer.yes).because "I said so"

def LongAnswer.eg₃ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₃ = ((LongAnswer.just ShortAnswer.yes).because "I said so").because "Did you not hear me?"

def LongAnswer.short : LongAnswer → ShortAnswer

The short answer to a long answer. Lean has convenient notation for pattern matching

Equations

• (LongAnswer.just ans).short = ans
• (ans.because reason).short = ans.short

def LongAnswer.short' : LongAnswer → ShortAnswer

The short answer to a long answer. Expanded definition

Equations

• (LongAnswer.just ans).short' = ans
• (ans.because reason).short' = ans.short'

def ShortAnswer.just (ans : ShortAnswer) : LongAnswer

The long answer from a short answer.

Equations

• ans.just = LongAnswer.just ans

def LongAnswer.justify (ans : LongAnswer) (reason : String) : LongAnswer

Adding a reason to a long answer.

Equations

• ans.justify reason = ans.because reason

def LongAnswer.eg₄ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₄ = ShortAnswer.yes.just.justify "I said so"

def LongAnswer.eg₅ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₅ = (ShortAnswer.yes.just.justify "I said so").justify "Did you not hear me?"

def LongAnswer.eg₆ : LongAnswer

An example of a term in the LongAnswer type.

Equations

• LongAnswer.eg₆ = ((ShortAnswer.yes.just.justify "I said so").justify "Did you not hear me?").justify "Please listen next time."

inductive EmptyAnswer : Type

There are no terms of this type.

• justified (and : EmptyAnswer) (reason : String) : EmptyAnswer

def EmptyAnswer.mapToType (α : Type) : EmptyAnswer → α

A function from EmptyAnswer to α for any type α. Such a function can only exist if EmptyAnswer has no terms.

Equations

• EmptyAnswer.mapToType α (prev.justified reason) = EmptyAnswer.mapToType α prev

noncomputable def EmptyAnswer.mapToType' (α : Type) : EmptyAnswer → α

A function from EmptyAnswer to α for any type α. Such a function can only exist if EmptyAnswer has no terms.

Equations

• EmptyAnswer.mapToType' α a = EmptyAnswer.rec (fun (prev : EmptyAnswer) (j : String) (ih : α) => ih) a

partial def EmptyAnswer.selfReference : EmptyAnswer