Re: [mizar] where do people check for the MML library?

["Miranda, Brando" <miranda9@illinois.edu>]

Hi Freek,

Thanks for the response.

I was hoping to learn the syntax by proving trial stuff, like in Coq, its helpful to even define natural numbers myself and define and prove properties about them, like n+m = m + n and other simple facts using even induction. 

is that possible in Mizar? Or is that a bad way to go about it?

I will read through it but I feel things don’t stick if I don’t actively do stuff. 

I am happy to write something up but I’d need to know what are the common practices, or the “Mizar way to code”.

Regards, Brando

> On Nov 29, 2018, at 5:25 PM, Freek Wiedijk <freek@cs.ru.nl> wrote:
> 
> Dear Brando,
> 
>> Interesting, so is that not the standard way to learn Mizar?
> 
> I don't know what the best way to learn Mizar is :-)
> 
> As for the "tutorial", what I would do if I were you is
> just read through it, and not really enter the specific code
> fragments into the system and ignore the exercises for now
> (as I wrote, they are outdated).  But hopefully the text
> will still help you understand the system a bit better.
> 
> And if you are into some interesting times, you _could_
> try to update the "tutorial" to make it up to date with
> respect to the current state of the system :-)  But of
> course, as Mizar is a moving target, that will soon be out
> of date again.
> 
> Freek