> A less ambitious goal which seems practically doable would be to allow
MM1 to import MM (this is another version of MM -> MM0 translation which
already exists), and then just produce small scale MM1 -> MM translations
like single theorems, using an approach similar to mmj2 or rumm where you
get some code blocks to copy into set.mm. If all the theorem statements are
written on the MM side then this solves most of the issues about variable
naming etc.
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?
> 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.)
--
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/8d85d99a-6ad3-4835-8285-386b5da5530an%40googlegroups.com.
