Defining a Separate Type underneath an Inductive

Stream: new members

[Colin Jones ⚛️]

I'm not sure how to ask this but how do I define a separate type underneath an inductive type. For example, I would like to define a TypeA type so the id_A function only takes inductive A instead of B or C.

inductive ABC
 | A | B | C
open ABC
deriving instance Repr for ABC

def id_A (input : "Type A") : ("Type A") :=
  match input with
  | A => A

Sorry if it's a silly question.

[Aaron Liu]

Do you want a subtype?

[Colin Jones ⚛️]

Yes maybe? If it works, I'll use it. I just want the function to deny other inputs that aren't A or a specific "category" of inputs from ABC.

[Aaron Liu]

This is what a subtype looks like

inductive ABC
 | A | B | C
deriving Repr

open ABC

def id_A (input : {a : ABC // a = A}) : {a : ABC // a = A} :=
  match input with
  | ⟨A, rfl⟩ => ⟨A, rfl⟩

[Aaron Liu]

You can also pass the proof to the function separately

inductive ABC
 | A | B | C
deriving Repr

open ABC

def id_A (input : ABC) (valid : input = A) : {a : ABC // a = A} :=
  match input with
  | A => ⟨A, rfl⟩