RECURSIVE FlatMap(_,_)
FlatMap(s,F(_)) == IF Len(s) = 0 THEN <<>> ELSE F(Head(s)) \o FlatMap(Tail(s), F)
I'll get an error:
Definition of FlatMap has different arity than its RECURSIVE declaration.
This is a similar error I was struggling with this morning when playing with SortSet. But making LTE the first parameter seems to work:
TestSet(n) == [key:1..n, val:{"x", "y"}]
RECURSIVE SortSet(_,_)
SortSet(LTE(_,_),S) ==
IF S = {} THEN <<>>
ELSE LET s == CHOOSE t \in S : \A u \in S : LTE(t, u)
IN <<s>> \o SortSet(LTE, S \ {s})
LL == SortSet(LAMBDA x,y : x.key <= y.key, TestSet(4))
Yuri