Zulip Chat Archive

Stream: new members

Topic: Constructing Types


Chase Norman (Dec 23 2020 at 22:06):

I have an existing fintype X. I would like to produce a Type that has all of the elements of X except a given element x. Is such a construction possible? If so, what route could I take to prove that the resulting type is a fintype? Thanks.

Yakov Pechersky (Dec 23 2020 at 22:26):

One simple way would be

import data.fintype.basic

variables {α : Type*} [fintype α] [decidable_eq α] {a : α}

example : fintype {x // x  a} := by show_term {apply_instance}

/-
Try this: exact subtype.fintype (λ (x : α), x ≠ a)

-/

Yakov Pechersky (Dec 23 2020 at 22:27):

Without the decidable_eq, you don't have a decidable procedure for knowing whether two elements are the same or not, so you don't know if an element is really in your subtype.

Eric Wieser (Dec 23 2020 at 23:30):

But you can always use open_locale classical if you don't care about computably enumerating the values


Last updated: Dec 20 2023 at 11:08 UTC