All Questions
Tagged with sigma-type lean4
1
question
7
votes
2
answers
767
views
Non-trivial examples of dependent sum ($\Sigma$-types) in Lean?
I am trying to understand the concept of dependent sum types ($\Sigma$ types) using concrete examples. The example given in Theorem Proving in Lean 4 seems to be a degenerate case rendering the ...
- 2,220