All Questions
Tagged with lean inductive-type
4
questions
5
votes
1
answer
149
views
Explain all the arguments to this rec eliminator
I defined this inductive type for representing JSON elements
...
- 273
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 ...
4
votes
1
answer
228
views
Making a finite graph type in Lean - introduction rule
I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
6
votes
2
answers
273
views
How to prove in Lean that sums are distributive?
Assume we are given three types in Lean.
constants A B C : Type
There is a canonical map of the following form.
...
- 722