Getting trace of the definitions defined on inductive types

Stream: new members

[Ayush Agrawal]

Hi guys, it would be really helpful if anyone could suggest a way to trace how the rec_on does the job of constructing correct terms. For example, doing #reduce nat.add (nat.succ nat.zero) (nat.succ (nat.succ nat.zero)) directly gives me 3 or (nat2.zero.succ.succ.succ) but it would be cool to see what's happening under the hood. Thanks!