mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Unify `char_zero` with `char_p`

Open urkud opened this issue 5 years ago • 0 comments

Proposed changes:

  • make p in char_p an out_param;
  • make it work for an add_monoid instead of a semiring;
  • use char_p α 0 instead of char_zero.

See Zulip

urkud avatar Oct 19 '20 12:10 urkud