> data Nat := (zero : Nat) ; (suc : Nat -> Nat) ;
Data'd.
 > let plus : (m : Nat) (n : Nat) : Nat ;
Parse failure: end of parser.
 > let plus (m : Nat) (n : Nat) : Nat ;
Let there be plus.
\ m : Nat ->
\ n : Nat ->
Programming: < plus^1 m n : Nat >
plus_1.plus-impl_2 > <= Nat.Ind n
Eliminated and simplified.
\ m^2 : Nat ->
\ n : Nat ->
\ m : Nat ->
Programming: < plus^1 m 'zero : Nat >
plus_1.plus-impl_2.makeE_2.m_1.s_0.e_0.xf_0.u_0.u_0 > = m
Ta.
\ m^2 : Nat ->
\ n : Nat ->
\ xf^1 : Nat ->
\ xf : (m : Nat) -> < plus^1 m xf : Nat > ->
\ m : Nat ->
Programming: < plus^1 m ('suc xf^1) : Nat >
plus_1.plus-impl_2.makeE_2.m_1.s_0.e_0.t_1.xf_0.s_0.u_1.s_0.u_1 >