Commit 2023-07-15 20:46 d5cc6ecd

View on Github →

fix: fix ZFC Basic module docstring (#5757) The Lean 3 names were not updated to Lean 4 in the module docstring. Also fix capitalisation in some declarations (Arity.const, PSet.Resp.evalAux, Classical.allDefinable).

Estimated changes

deleted def Arity.Const
added def Arity.const
modified theorem Arity.const_succ
modified theorem Arity.const_succ_apply
modified theorem Arity.const_zero
modified theorem PSet.Arity.equiv_const
deleted def PSet.Resp.EvalAux