Generic Types

Stream: Is there code for X?

[Chase Norman]

Here is a mwe of my current situation:

def Parameterized {X Y : Type} [fintype X] [fintype Y] := X → Y

structure S :=
  (F : Parameterized → set X)
  ...

My goal is for the F function within S to take any Parameterized and create a set using the same type X as the Parameterized uses for its type argument X. I've tried defining X and Y as example variables. I tried defining them as Sort (as is done in various mathlib files), but I could not construct a set with them. I've tried permuting between curly braces and normal parenthesis in the Parameterized definition. The answer has eluded me due to the type classes. How can I achieve my goal?

[Yakov Pechersky]

I would think you'd need to have (X Y : Type), otherwise it's not possible to infer what types Parameterized is over.

[Patrick Lutz]

This works for me

import data.fintype.basic

def Parameterized (X Y : Type) [fintype X] [fintype Y] := X → Y

structure S {X Y : Type} [fintype X] [fintype Y] :=
  (F : Parameterized X Y → set X)

Is that the kind of thing you want?

[Patrick Lutz]

This also works (and is not really any different from what I posted previously)

import data.fintype.basic

variables (X Y : Type) [fintype X] [fintype Y]

def Parameterized := X → Y

variables {X Y}

structure S :=
  (F : Parameterized X Y → set X)

[Patrick Lutz]

It may be easy to get confused when looking at mathlib for guidance as many files in mathlib have some line like variables (X Y : Type) [fintype X] [fintype Y] somewhere high up in the file: this line means that essentially every lemma/def/whatever later in the file also has the arguments (X Y : Type) [fintype X] [fintype Y] without having to write them explicitly. But this means that if you just look at one def or lemma statement later in the file you might be effectively missing part of the statement because you haven't looked at the line(s) in the file where various variables are declared