Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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 and 

NatInductiveDefConclusion 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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6FD26A6D-8D05-4C50-ADE6-130CD2B17A82%40gmail.com.