Re: [tlaplus] Functions and Operators

[Stephan Merz <stepha...@xxxxxxxxx>]

> For example, \in has type "'a set => bool"

That should (of course) have been "'a => ('a set => bool)". Incidentally, you can define "'a set" simply as an abbreviation for "'a => bool" in HOL, identifying sets and their characteristic predicate (and \in is just [reverse] function application). Then, you can define the set of all values of type 'a as

  UNIV :: "'a set" == \lambda x::'a. true

Note that there is a separate such set for every type, in particular

  (UNIV :: "'a set")    and    (UNIV :: "'a set set")

are different for any type 'a, and this helps avoiding paradoxes.

Stephan