Pretty Syntax for Operators on Abstract Structures

Stream: general

[Mridul Aanjaneya]

I'm a newbie in Lean. I was wondering how to define pretty syntax for mathematical operators on abstract structures? For example, if we consider the following typeclass:

class has_mul (\alpha : Type) where
  mul : \alpha -> \alpha -> \alpha

then I'd like to define a notation such that I can denote the pre-fix "mul" operator as an infix * operator.

Similarly, if I define another typeclass as follows:

class has_one (\alpha : Type) where
  one : \alpha

then I'd like to denote "one" as "1".

How can I achieve these? Thanks!

[Mridul Aanjaneya]

Nevermind! It looks like all the answers are here.