4.2.2: "def plus : nat → nat → nat | nat.zero m := m | (nat.succ n') m := nat.succ (plus n' m) " --> Where do the n and m come from? I'm assuming that m is the second argument and n is the first argument, because that makes the most sense with the problem. The comment given is good but there's no specific pseudocode to illustrate what exactly is happening.

[nehakrishnakumar]

Actually, it makes sense now, thank you!