Re: [isabelle] type inference in HOL

Quoting Stefan Berghofer <berghofe at>:

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.

ok, thanks. Still, the example I had in mind was:

 consA :: "('a*bool)"

 consB_def : "consB == snd consA"

I'd expect the following is logically safe:

 ALL x::singleton. snd (x,y) = ALL x::bool. snd (x,y)

The extra type variable is there, but it is simply not used.


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