Why is Nat.twoStepInduction a def but not a theorem?

Stream: new members

[Kevin Cheung]

Why is the two-step induction principle declared with def when strong induction principles are theorem? What advantages are there with using def? Could the strong induction principles have been declared using def as well?

def Nat.twoStepInduction {P : ℕ → Sort u}
    (H1 : P 0)
    (H2 : P 1)
    (H3 : (n : ℕ) → P n → P n.succ → P n.succ.succ)
    (a : ℕ)
  : P a

[Etienne Marion]

The difference between a theorem and a def is that a theorem can only output a Prop term, while a def can output data. In your particular case, twoStepInduction outputs P a : Sort u, so it can output data. In the case of strong induction however, the output always has type Prop, so it is a theorem.

[Etienne Marion]

But the def version also exists, it is docs#Nat.strongInductionOn

[Kevin Cheung]

Thanks.