Re: [isabelle] type inference in HOL



Quoting Stefan Berghofer <berghofe at in.tum.de>:

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) =
  False

which is an inconsistency.

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

 consts
 consA :: "('a*bool)"

 constdefs
 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.

Best,
Paolo







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