Commit 2023-01-21 14:33 6523b757

View on Github →

feat: port Data.W.Basic (#1743)

Estimated changes

added def WType.depth
added theorem WType.depth_pos
added def WType.elim
added theorem WType.elim_injective
added def WType.equivSigma
added def WType.ofSigma
added theorem WType.ofSigma_toSigma
added def WType.toSigma
added theorem WType.toSigma_ofSigma
added inductive WType