Theorem Nat.rec_eq_recC

Modification history

2023-05-28 05:00

Mathlib/Init/Data/Nat/Basic.lean

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

Deleted Nat.rec_eq_recC View on Github →

2023-01-20 17:48

Mathlib/Init/Data/Nat/Basic.lean

fix: make List.rec and Nat.rec computable (#1720) …

Added Nat.rec_eq_recC View on Github →