On Mon, May 26, 2025 at 2:10 AM Gino Giotto <[email protected]>
wrote:
> This works for me. Only concern: when you mention "another version of MM
> -> MM0 translation which already exists" I think you are referring to the
> Haskell translator that converts a MM file into a MM0 or MMU file. I tried
> that command, but the statements of the produced file are represented as
> trees, like this:
>
> --| The value of the divisor function at a prime power. (Contributed by
> Mario Carneiro, 17-May-2016.)
> theorem sgmppw {k: setvar} (A2 P N: class):
> $ wi (w3a (wcel A2 cc) (wcel P cprime) (wcel N cn0)) (wceq (co A2 (co P
> N cexp) csgm) (csu k (co cc0 N cfz) (co (co P A2 ccxp) (cv k) cexp))) $;
>
> The above statement looks really hard to read for me, so I'm ok with the
> latter proposal if I can work with the original set.mm notation in MM1
> (or at least something similar). Looking at the set.mm0 file in the
> examples it seems it should be possible
> https://github.com/digama0/mm0/blob/master/examples/set.mm0, but maybe it
> requires more work?
>
The issue is that set.mm notations are not compatible with the mm0 notation
system, and the current translation makes no attempt to translate
notations. This can be done in at least some cases automatically, but it
seems like a lot of work to tune the heuristics...
> Another possibility which I did not mention in that post is to add
> constraints to MM1 (or specifically mm0-rs) to allow it to operate in "MM
> mode", where certain things are disallowed to make translation easier. That
> makes more sense if your goal is to use MM1 to develop set.mm rather than
> embedding peano.mm1 et al into set.mm.
>
> What would the user get compared to the other approach? (Others might be
> interested, though for me, the "less ambitious goal" would be good already.)
>
Well in any case you will want to either avoid things that MM is bad at.
You also need to store alignment information somewhere no matter how you go
about it.
--
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 visit
https://groups.google.com/d/msgid/metamath/CAFXXJSu6Uy4UwTuCp3%3DN8B8-zpie6S0FuGpq820zvEVYhe3T2w%40mail.gmail.com.
