Zulip Chat Archive

Stream: general

Topic: empty class


Reid Barton (Apr 24 2018 at 01:12):

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 (Apr 24 2018 at 01:18):

Try

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

Reid Barton (Apr 24 2018 at 01:22):

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

Reid Barton (Apr 24 2018 at 01:22):

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

Simon Hudon (Apr 24 2018 at 01:23):

Thanks for the tip!

Simon Hudon (Apr 24 2018 at 01:24):

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 : )

Last updated: Dec 20 2023 at 11:08 UTC