Hi Bill,
| I'm only going to use the infix `same_side' as if I'd declared it it
| to have your type `point->line->point->bool', but how does HOL Light
| know that? I would have thought HOL Light would require instead
|
| let same_side_DEF = new_definition
| `! A B be point . ! l be line . A,B same_side l <=>
| ~(?X. (X on_line l) /\ Between(A, X, B))`;;
|
| or something, maybe
| ! A:point B:point l:line . [...].
You can certainly make the types explicit, something like this:
let same_side_DEF = new_definition
`!A:point B:point l:line. A,B same_side l <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
This is potentially useful for documentation and may be necessary
in some cases. However, everything inside `term quotations` undergoes
a type inference phase that will try to infer types based on known
types of constants appearing there. In this case, since "Between" and
"on_line" have known types (as of course do the logical connectives
like "<=>") the types of all the variables get determined and hence
the type of "same_side" follows without any annotations. The process
of type inference uses a variant of the Hindley-Milner algorithm that
is known from languages in the ML family like OCaml.
| My 13yo son can read my Hilbert paper better than I can, and he found
| a ton of errors by going through it line by line. My skills at
| math-paper-writing-error-detection don't work well at that (for math
| folks) excessively high level of detail. But HOL Light will keep me
| coding until it's correct!
I am impressed that you already have an efficient proof-checker! But
yes, HOL Light should be even more careful and pedantic than any
human.
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
