Mathematical diagrams in lean

Stream: new members

[Andre Popovitch]

I think lean has some built-in support for custom notations, but I'm kind of curious about the reverse. When writing a proof it would be cool to be able to add some example inputs and see how they change at different steps of the proof. Is something like that possible?

[Arthur Paulino]

Do you have a simplified example of how you think this would work?

[Yaël Dillies]

You sure can. Proofs are just functions. However I don't know how to integrate this with the goal state.