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`,
Michael, that's very helpful! You taught me something about term.ml, and
reminded me of that every HOL term is either a constant, a variable, a function
(abstraction) or a function application (combination). So pasting your code
into HOL Light gives the right answers:
let PrintTermType tm =
On 18 Dec 2013, at 04:21, Michael Norrish wrote:
> On 18/12/13 14:56, Bill Richter wrote:
>> I tried something like this when you first posted, but I didn't think to use
>> dest_comb. Do you have any general tips on how to recognize a term as say a
>> combination (which worked here) on an abstra
On 18/12/13 14:56, Bill Richter wrote:
> I tried something like this when you first posted, but I didn't think to use
> dest_comb. Do you have any general tips on how to recognize a term as say a
> combination (which worked here) on an abstraction (not here)?
Try using a match-expression:
ma
Thanks, Rob! This is helpful info:
In all the HOLs, you will find that the parser uses various
constants like [the SETSPEC definition] to represent derived
syntactic constructs (like set comprehensions) in terms of
primitive constructs (like conjunction and equality) in such a way
On 13 Dec 2013, at 03:51, Bill Richter wrote:
> Thanks, Rob! Can you explain how HOL4 performs the quantification with
> GSPEC? I would think that GSPEC would have to choose a fresh variable, and
> I've never understood how that's to be done, because you have know that your
> new fresh varia
Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC?
I would think that GSPEC would have to choose a fresh variable, and I've never
understood how that's to be done, because you have know that your new fresh
variable hasn't already been chosen. So I would think that t
On 7 Dec 2013, at 07:19, Bill Richter wrote:
> Rob, I think the answer to your interesting question involves more
> complicated set abstractions like {y + 6 | y < 0}. I think here we see the
> merit of the HOL Light invisible variables, as this simple proof shows:
>
> …
> I think that's co
Rob, I think the answer to your interesting question involves more complicated
set abstractions like {y + 6 | y < 0}. I think here we see the merit of the
HOL Light invisible variables, as this simple proof shows:
g `EMPTY = {y + 6 | y < 0}`;;
e(REWRITE_TAC[SETSPEC; GSPEC]);;
e(REWRIT
This is idle curiosity on my part about HOL Light: why are the constants that
support set comprehensions defined in such a way that the parser has to
generate an invisible bound variable? This results in surprising behaviour like:
# `{x | x > 9}` = `{x | x > 9}`;;
val it : bool = false
HOL4 def
10 matches
Mail list logo
