如何使用运算符获取TLA + / PlusCal中序列元素的总和？

Question

有一个想法写这样的东西：

Sum(seq) == 
  LET F[m \subseteq {seq[x]: x \in DOMAIN seq}] ==
    IF Head(seq) = <<>> THEN 0
    ELSE Head(seq) + F[Tail(seq)]
  IN F[seq]

..但它不能那样工作。

Answer 1

ASSUME seq # <<>>
LET seq == <<1,2,3,4,5,3,5>>
    Sum[ i \in 1..Len(seq) ] == IF i = 1 THEN seq[i] ELSE seq[i] + Sum[i-1]
IN Sum[Len(seq)]