Zulip Chat Archive

Stream: general

Topic: Flip inductive parameters


view this post on Zulip 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)

view this post on Zulip Simon Hudon (Jun 05 2018 at 02:55):

You can do

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

view this post on Zulip Simon Hudon (Jun 05 2018 at 02:56):

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

view this post on Zulip Nicholas Scheel (Jun 05 2018 at 02:57):

okay, that should work :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (Jun 05 2018 at 03:33):

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

view this post on Zulip Simon Hudon (Jun 05 2018 at 03:34):

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

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (Jun 05 2018 at 03:35):

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

view this post on Zulip 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