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

*From*: timsoethout@xxxxxxxxx*Date*: Wed, 25 Mar 2020 06:27:32 -0700 (PDT)*References*: <CABZ6pRfSwipHCO1kQ0T2JpiA8U3mA7mgza0Y9KR1_=2tA-y8JQ@mail.gmail.com> <D946CB70-82D9-4CD8-AC2D-55A21A217C7F@gmail.com>

Thanks!

-- I see. So `Append(seq, elem)` adds `elem` to the end of `seq`, but `Head(seq)` denotes the first.

I was somehow expecting that `Append` and `Head` where each other's duals, but this is not the case.

Thanks again for the quick response.

On Wednesday, March 25, 2020 at 2:19:38 PM UTC+1, Stephan Merz wrote:

Thanks again for the quick response.

On Wednesday, March 25, 2020 at 2:19:38 PM UTC+1, Stephan Merz wrote:

Hello,Head(seq) denotes the first element of a sequence, you want the last element. TryLast(seq) == seq[Len(seq)](assuming that the sequence is non-empty).StephanOn 25 Mar 2020, at 14:16, Tim Soethout <t...@xxxxxxxxxxxxxx> wrote:Hi,I'm using TLA+ for some modeling and TLC finds a counter example, but I don't understand why?This statement:`Len(committed[r1]) = (Len(committed[r2])+1) => Append(committed[r2], Head(committed[r1])) = committed[r1]`is FALSE, but I don't see how?The value of committed is `(r1 :> <<t1, t2>> @@ r2 :> <<t1>>)`.What I'm trying to do is: If committed[r1] is 1 shorter than committed[r2], check if the last element from committed[r1] appended to committed[r2] makes them equal.In this example case this should hold, right? What am I missing?Thanks for potentially helping me.Best regards,Tim--

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 .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ .CABZ6pRfSwipHCO1kQ0T2JpiA8U3mA 7mgza0Y9KR1_%3D2tA-y8JQ% 40mail.gmail.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/b32c9271-9b79-4088-8d46-05e1ceb80cf5%40googlegroups.com.

**References**:**[tlaplus] Question about evaluation of Sequences***From:*Tim Soethout

**Re: [tlaplus] Question about evaluation of Sequences***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Question about evaluation of Sequences** - Next by Date:
**Re: [tlaplus] Changing editor's font colors for numbers, logical symbols, etc in the spec** - Previous by thread:
**Re: [tlaplus] Question about evaluation of Sequences** - Next by thread:
**[tlaplus] Q about the Alternating Bit Protocol example** - Index(es):