Flip inductive parameters

Stream: general

[Nicholas Scheel]

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]

You can do

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

[Simon Hudon]

And make Bezier' a functor (or switch the names)

[Nicholas Scheel]

okay, that should work :)

[Nicholas Scheel]

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]

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

[Nicholas Scheel]

aha, thank you! it was using applicative.to_functor and applicative's default map :face_palm:

[Simon Hudon]

Do you by any chance have a functor and a applicative instance available in your context?

[Simon Hudon]

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

[Nicholas Scheel]

I get that :) and yes, I have functor and applicative, working on is_lawful_applicative

[Simon Hudon]

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