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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 21 Mar 2015 14:24:12 +0100*References*: <888ba871-f342-4159-8f60-5b055ee40813@googlegroups.com> <2556ED24-313D-4CDA-AD2C-ED3DAAD7D749@gmail.com>

> 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

**Follow-Ups**:**Re: [tlaplus] Functions and Operators***From:*Andrew Helwer

**References**:**Functions and Operators***From:*Andrew Helwer

**Re: [tlaplus] Functions and Operators***From:*Stephan Merz

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