Commit 2023-12-06 23:43 5e798324
View on Github →feat: allow pattern matching in set-builder notation (#8850)
Allow the use of pattern matching in set-builder notation. For example, { (m, n) : ℕ × ℕ | m * n = 12 } denotes the set of all ordered pairs of natural numbers whose product is 12.