About ">"...
It isn't really necessary as set.mm has done just fine without it with
negation and "<_", right ?
Still, the general public knows about > and >_ and will want to use them.
But they can, with the right tools.
I know of 2 aspects of maths : content and presentation.
You get that in mathml
So, imo, it is fine if set.mm only has "<" and if the tool has an option
to display "the negation of <_" as ">".
For example, in the video for mephistolus M6 (with different variable names)
I display the sum sum_ k e. ( 0 ... n ) ( x ^ k) with
\sum_{k\in\{0...n} x^k
But people will want to see and work with
\sum_{k=0}^nx^k
I thought about it and it is completely possible (still it requires an
improved version of the selection widget because, if you want to select
( 0 .. n) with a mouse, you end up selecting the whole sum with the
current version, but I thought about it, this is doable with some
additionnal control/display) :
presentational math is just an aspect/projection/shade of content maths.
There are many possible shades and selecting such a shade should be a
presentational option
now, as a tool writer, I really really love deduplication of
theorems/definitions.
Because it means half the memory and the time cost
And cost grows exponentially with the depth of automatic proof research
I am considering what to do about commutativity, etc.. also
If it is possible for the tool to get a decent job done with a unique
powerful theorem, that gets projected to many shades
like |- ( 5 x. 7 ) = ; 3 5
and |- ( 7 x. 5 ) = ; 3 5
I think I will go that way
But this is just my opinion and I actually don't really want to
interfere with the metamath/mm0 direction because :
As math teachers have to select a subset of a mathematical corpus to
teach students and to work with that,
Mephistolus will should/will have to do that too. And so, it should be
able to adapt to metamath/mm0 (and not the other way around)
Best regards,
Olivier
--
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/81e60d53-f15f-b890-fa4e-f4e50831351d%40gmail.com.
