[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Y2i <yur...@xxxxxxxxx>*Date*: Sun, 6 Dec 2015 12:45:38 -0800 (PST)*References*: <75f4c1c5-52ee-4f44-a2fa-8dbadc6599ec@googlegroups.com> <9150ba4f-c010-4695-93d5-9c9d7e9d5b33@googlegroups.com>

Thank you Leslie and Ron!

This is interesting. It is probably a bug in TLC because if I swap the order of the operators, like below,

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

**Follow-Ups**:

**References**:**Recursive definitions of higher-order operators***From:*Y2i

**Re: Recursive definitions of higher-order operators***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] TLA+ logic** - Next by Date:
**Re: Recursive definitions of higher-order operators** - Previous by thread:
**Re: Recursive definitions of higher-order operators** - Next by thread:
**Re: Recursive definitions of higher-order operators** - Index(es):