empty class

Stream: general

[Reid Barton]

What's the right way to declare an empty class (i.e., one with no fields) and an instance of it? I found that this works:

class C (α : Type)
instance : C unit := C.mk unit

but it seems oddly non-uniform that C.mk takes an explicit argument, and I'd prefer not to repeat it. I guess I could define

def mkC {α : Type} := C.mk α

but I figured I'd ask here

[Simon Hudon]

Try

class C (α : Type) :=
 mk {} ::
instance : C unit := C.mk

[Reid Barton]

That worked, thanks. Also the :: isn't needed.

[Reid Barton]

(But I also don't know what it does, so maybe I am missing something?)

[Simon Hudon]

Thanks for the tip!

[Simon Hudon]

It's just a degenerate case of a notation for structure definition that allows you to pick a different name than mk for the constructor:

structure foo :=
  my_cons ::
    (field1 : ℕ)
    (field2 : ℕ)