Commit 2022-11-07 03:20 8c70608d

View on Github →

feat: port Init.Data.Prod (#543) add #align prod Prod to Init.Data.Core should the align be in Init.Data.Prod instead?

Estimated changes

deleted theorem Prod.mk.eta
added theorem Prod.mk.eta