Chaining coercions example in Functional Programming book

Stream: new members

[Lars Ericson]

The #eval at the end of the Chaining Coercions example in the Coercions section Functional Programming book won't work unless you add deriving Repr to the inductive types like this:

inductive A where
  | a
deriving Repr  -- needed for #eval

inductive B where
  | b
deriving Repr -- needed for #eval

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

#eval coercedToB

[Alex J. Best]

@David Thrane Christiansen is probably the person this comment is relevant to. Note that the book is generated from working lean code, and that that line was not included due to the set-up here https://github.com/leanprover/fp-lean/blob/56422d4a279d6a74dcf6dc1f9eaa84227ea81f0c/examples/Examples/Classes.lean#L1553

[Kyle Miller]

In particular the deriving instance Repr for B a couple lines down is a way to derive instances after the fact

[David Thrane Christiansen]

While the section prior to this one says how to do the deriving instance that the text talks about, an introductory text shouldn't be asking readers to keep fresh things up in their minds like this - it would be good to invoke those lines directly in the text to refresh the concept.

I created an issue to track this: https://github.com/leanprover/fp-lean/issues/123

In the meantime, you can include the deriving instance Repr for B line that the text suggests, but does not write directly.

[David Thrane Christiansen]

Thank you for letting me know about this!