Commit 2022-03-14 18:58 c1c61d44

View on Github →

feat(data/W/constructions): add constructions of W types (#12292) Here I write the naturals and lists as W-types and show that the definitions are equivalent. Any other interesting examples I should add?

Estimated changes