Commit 2023-10-23 14:19 482fff77

View on Github →

feat(Logic/Function/OfArity): generalize the return type (#7859)

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Curry.lean

modified def Function.OfArity.curry

modified def Function.OfArity.curryEquiv

modified theorem Function.OfArity.curry_uncurry

modified def Function.OfArity.uncurry

modified theorem Function.OfArity.uncurry_curry

Modified Mathlib/Logic/Function/OfArity.lean

modified def Function.OfArity.const

modified theorem Function.OfArity.const_succ

modified theorem Function.OfArity.const_succ_apply

modified theorem Function.OfArity.const_zero

modified def Function.OfArity

modified theorem Function.ofArity_succ

modified theorem Function.ofArity_zero

Modified Mathlib/SetTheory/ZFC/Basic.lean

modified def PSet.Arity.Equiv

modified theorem PSet.Arity.equiv_const

modified def PSet.Definable.EqMk

modified def PSet.Definable.Resp

modified def PSet.Resp.eval

modified theorem PSet.Resp.eval_val