Commit 2023-10-19 20:25 50e35884

View on Github →

chore(Logic/Function/OfArity): rename Arity to Function.OfArity (#7772) Also puts it in a new file.

Estimated changes

added def Function.OfArity
added theorem Function.ofArity_succ
added theorem Function.ofArity_zero
deleted def Arity.const
deleted theorem Arity.const_succ
deleted theorem Arity.const_succ_apply
deleted theorem Arity.const_zero
deleted def Arity
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
deleted theorem arity_succ
deleted theorem arity_zero