nonzero integer

Stream: new members

[Holly Liu]

how do i get an element from a set of nonzero integers? i tried def nat_plus_0 := ℕ ∪ {0} and get the errors failed to synthesize type class instance for has_union and has_singleton

[Mario Carneiro]

nat already has a zero

[Mario Carneiro]

if you want to add another one though you should use with_zero nat

[Mario Carneiro]

types are not sets, they have different operators for combining them

[Holly Liu]

ok

[Eric Wieser]

Why are you asking for non-zero integers yet trying to spell "the naturals including zero"?

[Holly Liu]

oops i think i actually meant ℤ \ {0}

[Holly Liu]

so i think this is what i'm trying to do: def nonzero := ℤ \ {0} and i get failed to synthesize type class instance for has_sdiff and has_singleton

[Eric Rodriguez]

again, ℤ is a type, \ is an operation on sets

[Eric Rodriguez]

usually you'd do something like (n : ℤ) (h : n ≠ 0)

[Eric Rodriguez]

but you could go for (n : { x : ℤ // x ≠ 0}) too, but I'd advice against it

[Holly Liu]

whoops sorry

[Holly Liu]

thanks!