All Questions
1
question
1
vote
1
answer
111
views
Inductive types associated to instances of a structure in Lean
I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example.
In it I have a structure Graph. I want to ...
