def definition def or abbrev

`toNat3`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 117def toNat3 (p : Pattern 3) : ℕ :=

Definition body.

 118  (if p ⟨0, by decide⟩ then 1 else 0) +
 119  (if p ⟨1, by decide⟩ then 2 else 0) +
 120  (if p ⟨2, by decide⟩ then 4 else 0)
 121

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.