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
(ALL (x::unit) (y::unit). x = y) =
(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