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

# Re: [tlaplus] VIEW for Structure variable

• From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
• Date: Wed, 9 Jun 2021 21:32:21 -0700
• Ironport-hdrordr: A9a23:jzLE96CmORU1z7XlHeiVsceALOsnbusQ8zAXPh9KJW0sTiXIra3e5cjziyWf+VAssQIb6Jm90ci7MAXhHPtOjrX5Uo3SKTUO1FHYX72KqLGStAEJ9UXFh6hgPYkJSdk4NDSyNyk4sS7CiDPIV+rIueP3qZxA5t2uu0uE+GpRGuFdBmVCe3Sm+xZNNUh77PMCffL2l6433EvcCAsqg9yAdwM4tqr41q32ffTdEFA77jEciTVm5gnYloISfSLoryv3klt0sNIfGKv+8zARJJ/MjxkKoSWsklM7I64m++fJ+59mL+rJsPE8DnHUkQCibI9gXr2erFkO0amSAFtAqqiCn//RVP4Dp085t1vFw2qL5yDQlA018nfnxBuhnXf+rYjYSVsBeoB8rLMcSQHB404s+Ot31rlGtljp/KZ/PFf6hj3049WNazFG/3DE7EYKoKoolnRaFaEeZLVSoYFa3EQQPowHADuS0vFkLACwNrCh2Mpr
• References: <45ec189e-dbfe-4959-ae23-9701b3f01404n@googlegroups.com>


On 09.06.21 21:04, pfeod...@xxxxxxxxx wrote:



In TLC, we have the VIEW config where you choose which variables are important and which are auxiliary.


Let's say I have a variable Var of interest which is always a Structure, would it be too hard to do something like VIEW but where you say that, for this Var, TLC does not consider some keys for fingerprint (kinda like auxiliary keys)?



A VIEW *is a state function* (page 243 in Specifying Systems). In other words, any state-level^1 (unprimed) expression can be a view, such as <<[n \in SomeSubsetOfDOMAIN Var |-> Var[n], other, variables>>

Don't shoot yourself in the foot!

Markus

^1 TLC will keep you from defining a constant-level expression.

--
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/b248a902-30da-c689-66fd-9f48b00be94e%40lemmster.de.