> On Jun 6, 2023, at 7:33 AM, Humanities Clinic <[email protected]>
> wrote:
>
> With assistance on the Github repo page itself, I was able to solve the
> problem, appreciated it.
>
> I have found that both on the web pages of MPE and on the GraphML output from
> running, metamath-knife set.mm --time --export-graphml-deps deps.xml,
> dependencies between definitions are missing.
>
> For example, df-grp is defined in terms of the following constants:
> Mnd
> Base
> `
> +g
> 0g
> (And all other "primitive" constants" like { A. ...)
>
> Hence, each constant can be a node, and there can be an edge for each "used
> in the definition of" relation.
>
> Can this sort of graph be extracted from set.mm using metamath-knife, or be
> obtained by any other means?
I'm sure metamath-knife could be modified to do that.
Another approach, though a little painful, is that you could scrape the
generated HTML about set.mm to get this information.
I don't remember if metamath-exe has an option to list the constants in use
(other than when generating the HTML). It obviously *has* that information
internally.
--- David A. Wheeler
--
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/8D6DA1C8-5816-4C2B-95E8-9E4C1E4E4391%40dwheeler.com.
