# Zulip Chat Archive

## Stream: general

### Topic: Flip inductive parameters

#### Nicholas Scheel (Jun 05 2018 at 02:53):

Is there a way to flip the `Type`

and `ℕ`

parameters around so I can make this a functor?

inductive Bezier (β : Type) : ℕ → Type | point : β → Bezier 0 | curve : Π {n}, Bezier n → β → Bezier (n+1)

#### Simon Hudon (Jun 05 2018 at 02:55):

You can do

def Bezier' (n : ℕ) (β : Type) := Bezier β n

#### Simon Hudon (Jun 05 2018 at 02:56):

And make `Bezier'`

a functor (or switch the names)

#### Nicholas Scheel (Jun 05 2018 at 02:57):

okay, that should work :)

#### Nicholas Scheel (Jun 05 2018 at 03:27):

wat

invalid type ascription, term has type g <$> @Bezier'.curve α n (@pure (Bezier' n) (@Bezier'.has_pure n) α x) x = @Bezier'.curve β n (g <$> @pure (Bezier' n) (@Bezier'.has_pure n) α x) (g x) but is expected to have type g <$> @Bezier'.curve α n (@pure (Bezier' n) (@Bezier'.has_pure n) α x) x = ?m_1

#### Simon Hudon (Jun 05 2018 at 03:28):

try `set_option pp.all true`

before your proof. It will display all the implicit parameters, universe levels and expand notations

#### Nicholas Scheel (Jun 05 2018 at 03:33):

aha, thank you! it was using `applicative.to_functor`

and applicative's default map :face_palm:

#### Simon Hudon (Jun 05 2018 at 03:34):

Do you by any chance have a `functor`

and a `applicative`

instance available in your context?

#### Simon Hudon (Jun 05 2018 at 03:34):

If you're used to Haskell, you'll see that Lean does not ensure that instances are globally unique

#### Nicholas Scheel (Jun 05 2018 at 03:35):

I get that :) and yes, I have `functor`

and `applicative`

, working on `is_lawful_applicative`

#### Simon Hudon (Jun 05 2018 at 03:36):

I suggest you make sure that only one is available at any time

Last updated: May 13 2021 at 05:21 UTC