Re: [mizar] Strong Mizar wish: linking to consider

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Sat, Mar 09, 2002 at 11:08:57AM +0100, Freek Wiedijk wrote:
> 
> But even if my wish were implemented, you could just still do
> it the other way, couldn't you?  I mean that's not a reason
> _against_ it?  Or wouldn't you even like to read a proof by
> someone else that would use then-after-consider.

I have been thinking now and then (for the last 20 some years)
about a formatter for Mizar proofs, not just a pretty printer
but a formatter allowing for hierarchical viewing of Mizar texts.
I do not think that when I am writing a proof I should be overly
concerned with its readability - we need a tool to make
Mizar texts easier to read.  I have nothing against your proposal
for linking to starnge places - I just do not see myself using it much.

> I thought of one more reason for this.  Because then "let
> ... such that ..." would be more equivalent to "let ...;
> assume ..." and "assume that ... and ..." would be more
> equivalent to "assume ...; assume ...".  Now I write "let
> ...; assume ..." instead of "let ... such that ..." in order
> to be able to use "then".

Some people for linking purposes use stuff like
  assume
A: P1 & P2 & ... Pk;

I do not want to forbid this but we need a tool that will split this
assumption into single/multiple ones and introduce appropriate labels
where needed and then references to A would be replaced by appropriate
ones.

> And "thus now" for "hereby" no doubt :-)  Our tastes clearly
> differ.  That in its turn would not be interesting to me.

I am happy to differ with people as long as there are no other
arguments for the opinions besides personal tastes ;-)

-- 
Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr