Commit 2022-11-07 03:20 e68b0f56

View on Github →

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

  • Adds two notation declarations that present in lean 3 and Lean3port but not yet in mathlib4. The onFun notation is needed in Logic/Relation. I'm not sure whether the combine notation is ever actually used, but we should include it for consistency.
  • Updates the name of on_fun to onFun, to match the naming conventions in the mathport output.
  • Adds a docstring to combine to satisfy the linter.
  • Fixes a typo in another docstring: "calles"` -> "called".

Estimated changes

added def Function.onFun
deleted def Function.on_fun