Zulip Chat Archive

Stream: Is there code for X?

Topic: Generic Types


view this post on Zulip Chase Norman (Jan 10 2021 at 04:07):

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?

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 04:43):

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

view this post on Zulip Patrick Lutz (Jan 12 2021 at 05:35):

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?

view this post on Zulip Patrick Lutz (Jan 12 2021 at 05:41):

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)

view this post on Zulip Patrick Lutz (Jan 12 2021 at 05:44):

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


Last updated: May 17 2021 at 16:26 UTC