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. We will now see two other special cases before the general case. Thus, we see:

• Enumerated types
• Non-recursive Inductive types
• Recursive Inductive types

inductive ShortAnswer : Type

• yes : ShortAnswer
• no : ShortAnswer
• maybe : ShortAnswer

instance instInhabitedShortAnswer : Inhabited ShortAnswer

Equations

• instInhabitedShortAnswer = { default := ShortAnswer.yes }

instance instReprShortAnswer : Repr ShortAnswer

Equations

• instReprShortAnswer = { reprPrec := reprShortAnswer✝ }

instance instDecidableEqShortAnswer : DecidableEq ShortAnswer

Equations

• instDecidableEqShortAnswer x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def ShortAnswer.or (a b : ShortAnswer) : ShortAnswer

Equations

• ShortAnswer.yes.or b = ShortAnswer.yes
• a.or ShortAnswer.yes = ShortAnswer.yes
• ShortAnswer.maybe.or ShortAnswer.no = ShortAnswer.maybe
• ShortAnswer.maybe.or ShortAnswer.maybe = ShortAnswer.maybe
• ShortAnswer.no.or ShortAnswer.no = ShortAnswer.no
• ShortAnswer.no.or ShortAnswer.maybe = ShortAnswer.maybe

def wrongOr (a b : ShortAnswer) : ShortAnswer

Equations

• wrongOr a b = sorry

def ShortAnswer.not (a : ShortAnswer) : ShortAnswer

Equations

• ShortAnswer.yes.not = ShortAnswer.no
• ShortAnswer.no.not = ShortAnswer.yes
• ShortAnswer.maybe.not = ShortAnswer.maybe