0 + 0
     : nat
HI
     : nat