Sum[n \in Nat] ==
IF n = 0
THEN [m \in Nat |-> m]
ELSE [m \in Nat |-> Sum[n-1][m] + 1 ] Ok, i see. Instead of writing something like
IF n = 0
THEN m
ELSE Sum[n-1,m] + 1we write it as:
[m \in Nat |-> IF n = 0
THEN m
ELSE Sum[n-1][m] + 1 ]
which has type [Nat -> [Nat -> Nat]] and apply the same theorems to prove is well defined.Thank you.On Sunday, June 14, 2020 at 9:58:54 AM UTC-3, Stephan Merz wrote:Hello,I guess that these useful theorems need adapted versions to be used for recursive functions defined on multiple parameters (e.g. Sum[n, m \in Nat]where recursion is done on one parameter having the other fixed) because key theorems/definitions like RecursiveFcnOfNat andNatInductiveDefConclusion are written assuming single parameter functions. I'm right?.I recommend "currying" such functions, i.e. using functions of type [Nat -> [Nat -> S]] instead of [Nat \X Nat -> S] for TLAPS. Functions with several arguments are not or very badly supported at the moment (and this limitation has existed for far too long).Sorry,Stephan