Re: [mizar] Why do Mizar types have to be non-empty?

[Freek Wiedijk <freek@cs.kun.nl>]

Andrzej:

>BTW. Are you sure that your 'normal form' is a type, not an attribute?

I guess "normal" is an attribute, while "normal form" is a
type.  It's like "natural number": "natural" is an attribute,
but "natural number" is a type.

I want to be able to say "reserve n for Normal_form of R;"
(where "R" is some kind of reduction relation") and then
later "consider n such that ..."

See <http://www.cs.kun.nl/~freek/notes/newman.ps.gz> for a
proof where this seemed the most natural way to do things.
(In that particular example I gave "R" the attribute
"nf_inhabited", just to get around this.)

Freek