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

*From*: Igor Kim <biosckon@xxxxxxxxx>*Date*: Mon, 19 Oct 2020 03:43:22 -0700 (PDT)

Clarifying my fundamental (mis-)understanding :)

[ {0, 1} -> {2, 3} ] \* set of functions. evaluates to:

{ (0 :> 2 @@ 1 :> 2),

(0 :> 2 @@ 1 :> 3),

(0 :> 3 @@ 1 :> 2),

(0 :> 3 @@ 1 :> 3) }

(0 :> 2 @@ 1 :> 2) \* is a function from the set above

(0 :> 2 @@ 1 :> 2) \in [ {0, 1} -> {2, 3} ] \* evals to TRUE

(0 :> 2 @@ 1 :> 2)[1] \* evaluates to 2

<<3,2,1>>[1] \* sequence/ tuple is a function so this evals to 3

So far makes sense.

Now...

(0 :> 2 @@ 1 :> 2) \* What is function?

I am under impression that function is **set** of one-to-one relations. Which it does look like. So it is a **set**, but not a *proper* TLA+ set? E.g. I cannot do this:

SUBSET (0 :> 2 @@ 1 :> 2)

Thank you!

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/0c1c51bb-e38c-471d-8d74-b95155267750n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Functions and Sets***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] UTF-8** - Next by Date:
**Re: [tlaplus] Functions and Sets** - Previous by thread:
**Re: [tlaplus] UTF-8** - Next by thread:
**Re: [tlaplus] Functions and Sets** - Index(es):