Are inductive types the only types that can pattern-match?

Stream: general

[nrs]

Am trying to understand a bit more about how Lean works. In a type theory we use for example pi types to define inductive types, so inductive types are not the only possible types in a type theory. In the specific case of Lean, are inductive types the only ones that can be pattern-matched?

[Marcus Rossel]

There are only three kinds of types you can construct in Lean: pi types, type universes, and inductive types. Since the first two can't be pattern matched, inductive types are the only ones that can.

[nrs]

Marcus Rossel said:

There are only three kinds of types you can construct in Lean: pi types, type universes, and inductive types. Since the first two can't be pattern matched, inductive types are the only ones that can.

I see! I wasn't sure how much of Lean's type system is exhausted by inductive types, thank you very much for the answer!

[Etienne Marion]

Marcus Rossel said:

There are only three kinds of types you can construct in Lean: pi types, type universes, and inductive types. Since the first two can't be pattern matched, inductive types are the only ones that can.

Aren’t there quotient types too?

[Floris van Doorn]

And I guess you can "define" types using choice. But you can definitely not pattern match on those.

import Mathlib.Tactic

noncomputable def «Don'tDoThis» : Type :=
  Classical.choose (p := fun α : Type ↦ Nat.card α = 3) ⟨Fin 3, by simp⟩