Re: reductions in Mizar

Freek Wiedijk <[email protected]> writes:

> Ah, that's quite restrictive!  I wanted to tell my Coq
> friends about this (they always complain that Mizar has no
> reduction), but now I don't know whether I dare to :-)

I think it's an advantage that the strict subterm relation wears its
termination property on its sleeve.  I would find it unpleasant if a
the validity of a proof depended on the confluence of a non-trivial
reduction relation whose confluence I didn't understand or to which I
had no direct access.

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/