[tlaplus] Relations

Hi all,

Recently, I tried to extract some parts of my proofs on relations to a separate module and then realized an overlap with the existing modules.

In my case, I modeled relations as a binary operator over a set.
In the StdLib WellFoundedInduction.tla considers a relation as a set of pairs. Also, an operator OpToRel translates an operator to the set representation.
The CommunityModules repo contains Relation.tla, which represents relations as a binary function to booleans.

I wonder which representation should be considered the "main one"? It would be easier to consolidate results if a common base is clear.

Karolis

--
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 visit https://groups.google.com/d/msgid/tlaplus/656065f4-e111-40cb-9bb9-419751023507n%40googlegroups.com.