fintype instance singleton

Stream: new members

[Bjørn Kjos-Hanssen]

This works, but there must be an easier way to do supply a fintype instance for γ?

inductive γ : Type
| q : γ

instance my_inst : fintype γ := fintype.mk {γ.q} (
  show ∀ (x : γ), x ∈ {γ.q}, from
    λ x,
    have h1: x=γ.q, from γ.rec_on x (show γ.q = γ.q, from rfl),
    finset.mem_singleton.mpr h1
)

[Adam Topaz]

instance my_inst : fintype γ :=
⟨{γ.q}, by { rintro ⟨⟩, simp }⟩

[Yakov Pechersky]

import tactic.derive_fintype


-- or @[derive [fintype, decidable_eq]]
@[derive [fintype]]
inductive γ : Type
| q : γ

#check γ.fintype

[Yakov Pechersky]

@[derive fintype] is also valid syntax, since you're deriving only one instance

[Patrick Johnson]

If you also want unique instance:

import tactic

inductive γ : Type
| q : γ

instance : unique γ := ⟨⟨γ.q⟩, λ a, (a.rec_on rfl).symm⟩
instance : fintype γ := unique.fintype

[Patrick Johnson]

It gives you fintype, subsingleton and inhabited

[Bjørn Kjos-Hanssen]

Sweet... I probably want unique

[Bjørn Kjos-Hanssen]

I guess instead of using @[derive [fintype]] one can just use the pre-defined

inductive unit : Type
| star : unit