Hi Bill,
on 21/3/14 4:28 PM, Bill Richter <rich...@math.northwestern.edu> wrote:
> ... BTW where is the constant = defined in HOL Light? I see now that
> the line in bool.ml override_interface ("<=>",`(=):bool->bool->bool`);;
> just means that <=> is being defined as a synonym for = in this special
> case. In general = has type A->A-bool.
That's right, the line in bool.ml is just defining an alias. The constant
'=' is *declared* (there is a difference in meaning between the words
"declare" and "define") in fusion.ml, in the line that sets the ML binding
'the_term_constants' (approx line 206). The type constants 'bool' and 'fun'
are declared similarly in fusion.ml in the line that sets
'the_type_constants' (approx line 114).
Mark.
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
