dc65f03c41
the internal constructions for structural and well-founded recursion use plenty of `PProd` and `MProd`, and reading these, deeply nested and in prefix notation, is unnecessarily troublesome. Therefore this introduces notations ``` a ×ₚ b -- PProd a b a ×ₘ b -- MProd a b ()ₚ -- PUnit.unit (x,y,z)ₚ -- PProd.mk x (PProd.mk y z) (x,y,z)ₘ -- MProd.mk x (MProd.mk y z) ``` (This is part 1, the rest will follow in #4730 after a stage0 update.)
4 lines
179 B
Text
4 lines
179 B
Text
[1, 2, 3]
|
|
(2, 3)
|
|
trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']'
|
|
trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')', ')ₘ' or ')ₚ'
|