# Re: [tlaplus] How to generate a sequence from another sequence ?

Q. does [i \in 1 .. Len(files) |-> files[i].id] gives back a sequence ?

Q. Is there something like a REPL where i can try different statements of TLA+ to check the output ?

On Tuesday, 10 November 2020 23:17:42 UTC-8, Stephan Merz wrote:
As far as I can tell, your attempt failed because a sequence is a function whereas the construct [x \in S |-> ...] expects a set S. Why not simply

[i \in 1 .. Len(files) |-> files[i].id]

where files' is your input sequence?

Stephan

On 11 Nov 2020, at 06:03, Ashish Negi <thisismy...@xxxxxxxxx> wrote:

Hi

I have a sequence of records with field id`. I want to get a sequence of all ids from original sequence.

My first attempt was to try this :
[r \in some_sequence_of_records |-> r.id]

"The exception was a java.lang.RuntimeException
: util.Assert\$TLCRuntimeException: The domains of formal parameters must be enumerable.
The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty."

Q1. Is "some_sequence_of_records" a set with DOMAIN 1..Len(sequence) ?
Q2. What is wrong with my first try ?

Currently, i am using custom map and filter functions for the sequences.

RECURSIVE mapSeq(_,_,_)
mapSeq(seqs, M(_), result) ==
IF seqs = <<>>
THEN result
ELSE mapSeq(Tail(seqs),
M,

GetAllIds(files) ==
LET getId(r) == r.id
IN mapSeq(files, getId, <<>>)

Q3. Is there a better way ?

Thanks
Ashish

--
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 tla...@googlegroups.com.