Currently #126 only considers equations that appear in some implications, so this will require some change

It would also be nice to have a separate file that only lists the implications and anti implications on the equations defined just in Equations.lean

Recently, Equations 28393, 374794, and 5105 have appeared in the output of lake exe extract_implications breaking some of my tools as they expected all equations to be in AllEquations.lean (I parse out the ones that are commented there as well.) That's probably a fault of my tooling, but also a good reason to do this to make it easier. Everyone can load a JSON.

That also broke some of my tools. I could add a Lean script to extract the equations, what would be a good I/O for it?

If you mean an output format, just a JSON hash seems easy for everyone to consume. Are you thinking of including it in extract_implications or somewhere else?

I think extract_implications already does a lot of things, it's better to make another script.
By output format I meant how to describe the equations. Is something like {"Equation3": [0, [0, 0]], "Equation4": [0, [0, 1]]} good? Would it be better to have {"Equation3": "x = x ◇ x", "Equation4": "x = x ◇ y"}? Something else?

As a short term fix one can of course add these equations in commented form to AllEquations.lean, and also add a note sonewhere in CONTRIBUTING.md requesting that one add the commented equation to AllEquations.lean whenever adding a novel equation to Equation.lean as a courtesy.

I think extract_implications already does a lot of things, it's better to make another script. By output format I meant how to describe the equations. Is something like {"Equation3": [0, [0, 0]], "Equation4": [0, [0, 1]]} good? Would it be better to have {"Equation3": "x = x ◇ x", "Equation4": "x = x ◇ y"}? Something else?

Personally, I'd go for the simpler textual form since lots of tools just need to display them, but there's nothing stopping you from having it be "Equation3": { "text": "x = x", "ast": [0, [0, 0]] }

claim

disclaim

claim

propose PR #429

This PR depends on #427.

I get the following build error on lake exe export_equations on main:

error: ././././scripts/export_equations.lean:27:39: application type mismatch
  Json.arr fun h ↦ Subtype.map (fun x ↦ ?m.281 x) h laws
argument
  fun h ↦ Subtype.map (fun x ↦ ?m.281 x) h laws
has type
  (∀ (a : RBNode Name fun x ↦ Unit), RBNode.WellFormed Name.quickCmp a → ?m.273 ((fun x ↦ ?m.281 x) a)) →
    Subtype ?m.273 : Sort (max 1 ?u.261)
but is expected to have type
  Array Json : Type
error: ././././scripts/export_equations.lean:27:52: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor
  RBNode Name fun x ↦ Unit
error: Lean exited with code 1
Some required builds logged failures:
- scripts.export_equations
error: build failed