Recursive definition in `Expr`

Stream: lean4

[Mathis Bouverot-Dupuis]

Hello ! I'm building some terms in Expr, and in particular I would like to define a recursive function. I'm having a hard time using recursors (.rec, .recOn, etc).

1. What is the complete list of recursors which are automatically defined for an inductive ?
2. Is there a way to do this with a higher-level API than recursors ?

[Eric Wieser]

You can write

def foo (e : Expr) : Nat :=
  match e with
  | .proj _ _ => sorry
  | .app f a => foo f + foo a
-- etc

[Henrik Böving]

I think Mathis means generating an Expr that represents a recursive function

[Mathis Bouverot-Dupuis]

Henrik Böving said:

I think Mathis means generating an Expr that represents a recursive function

Yes exactly.

[Eric Wieser]

I guess my suggeston then becomes "can you emit Syntax and elaborate it, rather than building an Expr"?

[Mathis Bouverot-Dupuis]

I would prefer not as I use some Expr-related machinery to build my terms, such as unification or local declarations. Is there a way to stay in Expr ?

[Eric Wieser]

By Expr-related, do you mean TermElabM-related?

[Eric Wieser]

You can jump back and forth between Expr and Syntax using docs#Lean.Expr.toSyntax and docs#Lean.Elab.Term.elabTerm

[Mathis Bouverot-Dupuis]

Eric Wieser said:

By Expr-related, do you mean TermElabM-related?

Yes, I'm using TermElabM and MetaM.

[Mathis Bouverot-Dupuis]

I see, so how would I use Syntax to build a match expression ? EDIT : a recursive definition (I was thinking about fixpoints)

[Eric Wieser]

Can you give an example of the kind of expression you want to build?

[Mathis Bouverot-Dupuis]

I would like to build something like this :

def myListMap (f : α → β) (xs : List α) : List β :=
  match xs with
  | [] => []
  | x :: xs => f x :: myListMap f xs

[Eric Wieser]

import Lean

open  Lean Meta Elab Term

def foo : TermElabM Expr := do
  let stx ← `(term|
    let rec myListMap {α β} (f : α → β) (xs : List α) : List β :=
      match xs with
      | [] => []
      | x :: xs => f x :: myListMap f xs
    myListMap)
  elabTerm stx none

[Mathis Bouverot-Dupuis]

With your definition foo, I tried inspecting the resulting term :

#eval do
  let e ← instantiateMVars =<< foo
  IO.println s!"{ ← ppExpr e }"

And I get (fun myListMap ↦ myListMap) ?m.16. How come the result has unassigned metavars ?

[Eric Wieser]

I think that metavariable is one satisfying docs#Lean.Elab.Term.isLetRecAuxMVar

[Eric Wieser]

I think the idea is that once you finally add the declaration to the environment, the let rec is added at the same time and the metavariable resolved; but I've not tried using let recs in meta code before