syntax for inductive type

Stream: lean4

[Jakob von Raumer]

Is it somehow possible for an inductive type Foo to easily derive a simple printing and a partial parsing function to and from Syntax that roundtrips when starting with an instance of Foo?

[Eric Wieser]

Mathlib has deriving ToExpr; does that help?

[Eric Wieser]

For example:

import Mathlib

inductive Foo
| one : Foo
| two (F : Foo) : Foo
deriving Lean.ToExpr, Repr


open Lean PrettyPrinter Elab Term Meta
#eval do
  delab <| Lean.toExpr (Foo.two Foo.one)

open Qq
#eval do
  let x ← evalExpr Foo q(Foo) <| ← elabTerm (← `(Foo.two Foo.one)) (some q(Foo))
  Lean.logInfo f!"{repr x}"

[Jakob von Raumer]

Oh, thanks I think evalExpr was the piece I was missing actually!

[Jakob von Raumer]

I thought there might be some functions to do it without going via Expr