mathlib3

c1c61d44 - feat(data/W/constructions): add constructions of W types (#12292)

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? Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>