Zulip Chat Archive

Stream: new members

Topic: fintype instance singleton


Bjørn Kjos-Hanssen (Aug 02 2022 at 20:16):

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 (Aug 02 2022 at 20:20):

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

Yakov Pechersky (Aug 02 2022 at 20:20):

import tactic.derive_fintype


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

#check γ.fintype

Yakov Pechersky (Aug 02 2022 at 20:22):

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

Patrick Johnson (Aug 02 2022 at 20:24):

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 (Aug 02 2022 at 20:27):

It gives you fintype, subsingleton and inhabited

Bjørn Kjos-Hanssen (Aug 02 2022 at 20:27):

Sweet... I probably want unique

Bjørn Kjos-Hanssen (Aug 06 2022 at 03:41):

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

inductive unit : Type
| star : unit

Last updated: Dec 20 2023 at 11:08 UTC