That's a very nice introduction (although a bit fast for me when describing
tactics). I like the explicit dichotomy between the proof assistant, that
may be large with many features, versus the proof verifier, that has to be
minimal.
I was wondering how "delimiter" works. Can there be middle delimiters ?
For instance, if I want to allow expresions like {x|ph}, should I write
delimiter ${$ $|$ $}$;
or
delimiter ${ |$ $} |$;
Secondly, is it one line per matching pair of delimiters or a single line
for all of them:
delimiter $($ $)$;
delimiter $[$ $]$;
versus
delimiter $( [$ $) ]$;
Probably the latter, considering your example
delimiter $( ~$ $)$;
And lastly, can I have multi-character delimiters like
delimiter $\[$ $\]$;
or the even more ambiguous
delimiter $(( ($ $)) )$;
I understand that the tokenizer puts an implicit space after every left
delimiter and before every right delimiter, but in the last case I am not
sure what it does.
Compared with Metamath, the "|-" type has been replaced with the "provable"
qualifier. I am not sure I see all the implications. For instance,
Metamath has to prove that longer expressions are well-defined, e.g. it has
to prove "wff ( ph -> ph )" before proving "|- ( ph -> ph )" (it does it
implicitly in the non-essential steps, but this can be made explicit, see
e.g. http://us.metamath.org/mpeuni/bj-0.html). How does this translate in
MM0 ?
A smaller thing: I would have said that the opposite of "public" is
"private", not "local", but there might be a reason why you chose the
latter term ?
Thanks,
Benoît
On Tuesday, January 5, 2021 at 6:38:41 PM UTC+1 [email protected] wrote:
> Hi All,
>
> I've finally gotten around to writing a tutorial on MM0 and mm0-rs for the
> lean together conference this year. Perhaps it will help situate it with
> respect to other metamath-based theorem provers in terms of feature set.
>
> https://www.youtube.com/watch?v=A7WfrW7-ifw
>
> Mario
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/f7598077-7efe-4b19-808c-043b967f0d64n%40googlegroups.com.
