Understanding extract_implications outcomes

Stream: Equational

[Eric Taucher]

Working though understanding list_outcomes in https://github.com/teorth/equational_theories/blob/main/equational_theories/Closure.lean#L346-L369. Since the arrays are really really large and very hard to view was thinking it might be easier if instead of working with magma upto order 4 if extract_implications had an option to accept the order value as an option. I don't expect anyone to make the changes but just want to check that the only things that need to be adjusted are the input from the two files

• equations.txt
• duals.json

I also realize that EquationalResult.lean could use another value to hold the size of the order
or to filter out items from the list based on the attribute in extract_implications before processing.

Thanks.

[Vlad Tsyrklevich]

What's the use case? Order can just be determined by the number of the equation

[Eric Taucher]

Vlad Tsyrklevich said:

What's the use case?

Just trying to understand extract_implications outcomes.

[Vlad Tsyrklevich]

if it would make your life easier if the input is shorter, it would be easiest to truncate the list to only the first N elements to Closure.list_outcomes, though you may not get as many transitive implications in that case