All Questions
Tagged with lean inductive-type
1
question
4
votes
1
answer
229
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&...
