Count tree leaves

2/4 ~20 minlean

Complete the recursive leaf count.

7 lines · Lean 4

inductive Tree (α : Type) where
  | leaf (value : α)
  | branch (left right : Tree α)

def leaves : Tree α → Nat
  | .leaf _ => sorry
  | .branch l r => sorry

Objectifs

Complete the recursive leaf count.

Indices

Voir la solution

inductive Tree (α : Type) where
  | leaf (value : α)
  | branch (left right : Tree α)

def leaves : Tree α → Nat
  | .leaf _ => 1
  | .branch l r => leaves l + leaves r