Hi Bill,
| let Collinear_DEF = new_definition
| `Collinear(A, B, C) <=>
| ?l. A on_line l /\ B on_line l /\ C on_line l`;;
|
| (* Error message for Collinear is
| Exception: Failure "typechecking error (initial type assignment)".
All HOL Light infixes are assumed to be curried at the outer level,
so HOL Light is expecting to typecheck "A on_line l" as
"((on_line) A) l". If you change the earlier line to the following,
it will work:
new_constant("on_line",`:point->line->bool`);;
| If I evaluate some other code first, the beginning of my Tarski code,
| however, I get no error message. So start a HOL Light session over:
In this case "on_line" is being defined, and when parsing the term used
in the definition, the "on_line" constant ends up getting the expected
curried type.
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
