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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Thu, 11 May 2017 14:08:21 +0200*References*: <CAMDXC8KdhqUTyU35hVbWYFqsCZy6gMspqAH5N6tMm4E3u7Ompg@mail.gmail.com> <1A886A09-E833-4CF4-8DA8-23CFFF4C6464@gmail.com> <b60079f6-ec32-3b61-6ddf-25f25700c299@gmail.com>

Hi Ioannis,
I am unable to reproduce this issue. For example, SANY accepts LEMMA ASSUME NEW S, NEW e(_,_), IsFiniteSet(S) PROVE LET f == [x \in S \X S |-> e(x[1], x[2])] IN \A x \in S : IsFiniteSet({f[x,y] : y \in S}) Could you please expand? Stephan |

**Follow-Ups**:**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

**References**:**Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Stephan Merz

**Re: [tlaplus] Arity of NEW operator in `tlapm`***From:*Ioannis Filippidis

- Prev by Date:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Next by Date:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Previous by thread:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Next by thread:
**Re: [tlaplus] Arity of NEW operator in `tlapm`** - Index(es):