Definitionally unfolding a term with holes

Stream: lean4

[Kevin Fisher]

Is there an easy way to definitionally unfold a term in lean4? I tried using #eval, but I can only get it to work on terms where I don't have any variables that range over a type, I tried adding a function but I don't think eval can show it in that case. Basically, I want to know what form lean will reduce a term to for the purposes of a reflexivity comparison.

This is my code:

def iter (c0 : α) (cs : α → α) : Nat → α
  | 0   => c0
  | n+1 => cs (iter c0 cs n)

def pred (n : Nat) : Nat :=
  Prod.fst (iter (0, 0) (λ (_, n) => (n, Nat.succ n)) n)

def nat_rec (c0 : α) (cs : Nat → α → α) (n : Nat) : α :=
  iter c0 (cs (pred n)) n

And the things I'm trying to expand are nat_rec c0 cs (Nat.succ (Nat.succ n)) and cs (Nat.succ n) (nat_rec c0 cs (Nat.succ n))

[Kevin Fisher]

Nevermind, I found it, it's #reduce