singleton.vh

-- Say we want to represent the smallest non-zero
-- positive number.  Call it omega.

RealPos = filter (> 0) Real \ [0]

-- Try one (1):
omega_1 = index 0 <| collect [ n : Real => 0 < n < m => m <- RealPos ]
-- This is not quite so great, this will collect the elements
-- into a vector, and since its a singleton, get the first and only
-- element.  This elememt will be computed after a while, and we'll
-- get the smallest non-zero, positive 64bit floating-point number.

-- This is not satisfactory, we want to mathematically represent
-- this concept.

-- Try two (2):
omega_set = [ n : Real => 0 < n < m => m <- RealPos ]

-- Verify that this set is indeed a singleton.
assert (singleton? omega_set)  --> :true

-- Extract the singleton:
omega_2 = singleton omega_set

-- or even better, with a pattern match.
[ omega ] = [ n : Real => 0 < n < m => m <- RealPos ]

assert (omega_2 == omega)


-- Simpler examples:
a : Nat
[ a ] = [ n : Nat => 1 < n < 3 ]

assert (a == 2)


assert (singleton? [ n : Nat  => 2 < n < 4 ] == :true)
assert (singleton? [ n : Real => 2 < n < 4 ] == :false)