Mathlib v3 is deprecated. Go to Mathlib v4

Def opt_param.out

Modification history

2022-04-22 12:15

src/logic/basic.lean

feat(logic/basic): add `auto_param.out` and `opt_param.out` (#13599)

Added opt_param.out View on Github →