nice way to implement instances on mutually defined types?

Stream: new members

[JJ]

I have the following code that implements ToString for a simple Expr type:

def Index := Nat
deriving ToString

inductive Expr where
| abs (body : Expr)
| app (func arg : Expr)
| var (idx : Index)

instance : ToString Expr := ⟨toString⟩
where toString
| .abs body => s!"(λ {toString body})"
| .app func arg => s!"{toString func} {toString arg}"
| .var idx => s!"{idx}"

I'm pretty happy with the aesthetics of this code. The where declaration lets the toString helper avoid polluting the namespace. On the other hand, with mutually-defined inductive datatypes, I can't seem to avoid ugly naming conventions:

mutual
inductive Value where
| clos (body : Expr) (env : Array Value)
| ntrl (neutral : Neutral)

inductive Neutral where
| nvar (idx : Index)
| napp (func : Neutral) (arg : Value)
end

mutual
def toString_Value : Value -> String
| .clos body _ => s!"(λ {body})"
| .ntrl neutral => toString_Neutral neutral
def toString_Neutral : Neutral -> String
| .nvar idx => s!"{idx}"
| .napp func arg => s!"{toString_Neutral func} {toString_Value arg}"
end

instance : ToString Value := ⟨toString_Value⟩
instance : ToString Neutral := ⟨toString_Neutral⟩

Does anyone have suggestions for how to clean this code up?

[Aaron Liu]

I would call those Neutral.toString and Value.toString

[JJ]

Oh, it slipped my mind I could just name them that. Thanks. No way to get around the mutual block, right?

[Kyle Miller]

Using a mutual block is the standard way to write these.

By the way, it's usually better having a separate def, rather than pack everything into the instance. Last I checked, the compiler will eagerly unfold instances, which causes much more inlining than you'd expect. That means slower compilation and larger binaries, if that matters to you.