Def Function.onFun

Modification history

2024-05-07 01:05

Mathlib/Init/Function.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Function.onFun View on Github →

2023-07-14 19:11

Mathlib/Init/Function.lean

chore: re-port Init.Function (#5859) …

Modified Function.onFun View on Github →

2022-11-07 03:20

Mathlib/Init/Function.lean

feat: port `onFun` and `combine` notations in Init.Logic (#542) …

Added Function.onFun View on Github →