Re: [isabelle] type inference in HOL
paolot at informatik.uni-bremen.de wrote:
Do you know if it is generally the case that unistantiated variables
lead to inconsistencies?
If you were allowed to make the following definition
singleton :: bool
"singleton == (ALL (x::'a) (y::'a). x = y)"
which has an extra type variable 'a on the right-hand
side, you could derive
(ALL (x::unit) (y::unit). x = y) =
(ALL (x::bool) (y::bool). x = y) =
which is an inconsistency.
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and