Def Prod.recC

Modification history

2023-05-28 05:00

Mathlib/Init/Data/Prod.lean

feat: add `compile_inductive%` and `compile_def%` commands (#4097) …

Deleted Prod.recC View on Github →

2023-04-20 10:27

Mathlib/Init/Data/Prod.lean

feat: port Data.Seq.Parallel (#3512) …

Added Prod.recC View on Github →