Re: [mizar] Private DB

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi Freek,

> Coq allows empty types.  PVS allows empty types.  So it is
> possible to allow empty types and still have a moderately
> useful system.  Or do you think that those systems are not
> sound? :-)
No,  I don't think so. :)

>http://mizar.uwb.edu.pl/cgi-bin/wilma/wilma_glimpse/mizar-forum?query=empty+types&Search=Search&errors=0&maxfiles=50&maxlines=10&.cgifields=filelist&.cgifields=partial&.cgifields=restricttofiles&.cgifields=case&.cgifields=lineonly

Yes, I see, there was a long thread on this topic.

Michael