Getting magma laws in MetaM

Stream: Equational

[Adam Topaz]

I tried looking for some (meta) code that obtains a term of MagmaLaw corresponding to an equation given by a n : Nat (assuming Equationn is in the environment). Does the repo already have something like this? If not, I wrote some code that does this that I will be happy to PR.

[Shreyas Srinivas]

It's either the EquationCommand or FactsSyntax

[Shreyas Srinivas]

Depending on what you want

[Shreyas Srinivas]

EquationCommand produces MagmaLaws

[Shreyas Srinivas]

FactsSyntax can be used to provide large classes of implications/anti-implications by referring to lists of Nat numbers of the equations

[Shreyas Srinivas]

It is possible that there is no exact function that returns the name of the equation given a number but FactsSyntax needs to translate those Nats to equation names, and so contains code you could use.

[Adam Topaz]

Okay, I see they're just all stored in the env extension associated with magmaLawExt.

[Shreyas Srinivas]

By the way Anand tried to add the laws into some environment extension last week and this significantly slowed CI run time. Do please look into that thread. I have forgotten the details

[Shreyas Srinivas]

https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/slow.20build/near/475869383

[Shreyas Srinivas]

(deleted)

[Mario Carneiro]

That issue is fixed, the current version of the equation command adds everything to the extension

[Andrés Goens]

I'm confused about the given an n : Nat? Is this the number of the equation? there is this draft PR https://github.com/teorth/equational_theories/pull/322 but I don't know it'll ever be used. As others pointed out we instead do that when elaborating equation and build both at the same time