Zulip Chat Archive

Stream: new members

Topic: How do I make a one out of a set


view this post on Zulip Lars Ericson (Dec 13 2020 at 05:20):

I want to make a set X be it's own 1 for the type set X. This isn't working, what's the right way?

import data.finset.basic
def X := fin 3
instance X_has_one : has_one X := fin.has_one
instance PX_has_one : has_one (set X) := { one := X }

The error message is

type mismatch at field 'one'
  X
has type
  Type : Type 1
but is expected to have type
  set X : Type

and I don't know what to make of this.

view this post on Zulip Heather Macbeth (Dec 13 2020 at 05:56):

The set of all elements of the type X is given by set.univ.

instance PX_has_one : has_one (set X) := { one := set.univ }

view this post on Zulip Lars Ericson (Dec 13 2020 at 14:40):

Thank you @Heather Macbeth that works!

import data.finset.basic
def X := fin 3
instance PX_has_one : has_one (set X) :=
{ one := set.univ }

Last updated: May 08 2021 at 19:11 UTC