Re: [isabelle] type inference in HOL

paolot at 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

  True =
  (ALL (x::unit) (y::unit). x = y) =
  singleton =
  (ALL (x::bool) (y::bool). x = y) =

which is an inconsistency.


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.