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?StephanOn 11 Nov 2020, at 06:03, Ashish Negi wrote:HiI 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 nestedexpressions 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,                    Append(result, M(Head(seqs))))GetAllIds(files) ==    LET getId(r) == r.id    IN mapSeq(files, getId, <<>>)Q3. Is there a better way ?ThanksAshish -- 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5f09aa29-391f-49f1-833f-c6200fa2450co%40googlegroups.com. -- 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/16E42E2A-E445-4194-AC25-859EA488D2C2%40gmail.com.