mutually recursive structures

Stream: general

[Tesla Zhang]

I want to create a couple of mutually recursive structures, but looks like I have to desugar them into inductives, according to the following error message I get:
image.png

is that true? Or am I missing something?

[Tesla Zhang]

The following code works, after I change structures to inductives:

import Lean
import Lean.Data.Json.Basic
import Lean.Data.Json.Parser
import Lean.Data.Json.Printer

namespace Canonical
open Lean Json ToJson FromJson

mutual
  inductive Bind : Type
  | mk (name : String) (type : Pi)
  inductive Pi : Type
  | mk (params : List Bind) (body : Option App)
  inductive App : Type
  | mk (head : String) (children : List Lam)
  inductive Lam : Type
  | mk (names : List String) (body : App)
end

end Canonical

But trying to derive Json things make it not work:

deriving instance ToJson, FromJson for Bind, Pi, App, Lam

[Tesla Zhang]

I think, it looks like Lean generates the json conversion functions, but did not mark them as mutually recursive:

image.png

[Tesla Zhang]

Using Szumi's trick the ToJson works, but FromJson doesn't because it doesn't really understand indexed families:

inductive Tag | bindT | piT | appT | lamT
open Tag
inductive Canon : Tag → Type
| bind (name : String) (type : Canon piT) : Canon bindT
| pi (params : List (Canon bindT)) (body : Option (Canon appT)) : Canon piT
| app (head : String) (children : List (Canon lamT)) : Canon appT
| lam (names : List String) (body : Canon appT) : Canon lamT
deriving instance ToJson, FromJson for Canon

image.png

[Tesla Zhang]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22default.20handlers.22.20when.20deriving.20DecidableEq/near/275722237

Looks like you'll need to add special support for it

[Tesla Zhang]

How does deriving work? Maybe I can do something about it...

[Tesla Zhang]

Qiu told me about where the functions are, it's mkToJsonInstance and mkFromJsonInstance, but they're are somewhat involved... Hmmm...

[Tesla Zhang]

https://github.com/leanprover/lean4/issues/4182