Recursive Functor map definition

Stream: lean4

[James Sully]

Hi, I have the following:

instance : Functor BinTree where
  map f t := match t with
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (map f l) (f x) (map f r)

This gives unknown identifier 'map'. With Functor.map instead, I get failed to synthesize instance Functor BinTree. How do I write a recursive typeclass method?

[Henrik Böving]

You implement it is a separate function and provide the instwce to the type class mechanism

[Henrik Böving]

But it would indeed be very cool if this worked ^^

[James Sully]

ah, thanks very much

[James Sully]

yep that worked

[James Sully]

I don't hate that to be honest, it feels organised to have a separate named map in the relevant namespace for each type

[Alex Keizer]

If for some reason you don't want to add a separate definition, you can also make do with

let rec map := fun f t => ...

[James Sully]

ah, I wasn't aware you could have a let immediately inside an instance where

[Alex Keizer]

Ah, no you can't. It would be:

instance : Functor BinTree where
  map :=
    let rec map := fun f t => ...
    map