Bill,
On 27 Dec 2013, at 18:47, Bill Richter wrote:
> ...
> Now this last part surprised me. I didn't know that numerals are
> combinations, and I would have guessed they were constants. So let me
> practice my is_*/dest_* skills:
>
> dest_comb `1`;;
>
> val it : term * term = (`NUMERAL`,
Here are a few observations about the set comprehension syntax in HOL Light and
HOL4.
The HOL4 Description manual says that {t | p} parses to: GSPEC(\(x1,. .
.,xn).(t,p)) where x1, . . . , xn are those free variables that occur in both t
and p. It also says that it is an error if there are no such
Hi Rob,
The code for HOL4 set abstractions says that the bound variables
of a set abstraction {t | p} are the intersection of the free variables
of t and p unless either side has no free vars, in which case the
bound variables are those of the other side. Also, if t has no free vars,
then fail.
Konrad,
On 29 Dec 2013, at 17:31, Konrad Slind wrote:
> Hi Rob,
>
> The code for HOL4 set abstractions says that the bound variables
> of a set abstraction {t | p} are the intersection of the free variables
> of t and p unless either side has no free vars, in which case the
> bound variables
