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

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

OK. But what it means if the type  'a normal form'  is empty. You need
the denotation for fixed variables, at least in standard semantics, in
which they are simply  local constants.

Greetings,
Andrzej

Freek Wiedijk wrote:

> Dear Andrzej,
>
> I thought a second more about this: "let t be a normal form"
> seems to have a different sentence structure from "let t be a
> term that is in normal form".
>
> Freek