Expr equations compiler

Stream: lean4

[Cody Roux]

I remember seeing a function in the standard lib that could take a recursively defined Expr and compile it into a definition, but for the life of me I cannot remember what it was called or how to find it. Does someone know?

[Robin Arnez]

Do you mean docs#Lean.Elab.addPreDefinitions​?

import Lean
import Qq

inductive Test (α : Type u) where
  | leaf (x : α)
  | branch (left right : Test α)

open Lean Meta Elab Qq

run_elab
  let u : Level := .param `u
  let self : Q({α : Type u} → Test α → Nat) := .const `Test.depth [u]
  let type := q({α : Type u} → Test α → Nat)
  let value : Q({α : Type u} → Test α → Nat) := q(
    fun t => t.casesOn (fun _ => 0) (fun l r => max ($self l) ($self r) + 1)
  )
  addPreDefinitions ({}, {}) #[{
    ref := .missing
    kind := .def
    levelParams := [`u]
    modifiers := {}
    declName := `Test.depth
    binders := .missing
    type := type
    value := value
    termination := {
      ref := .missing
      terminationBy?? := none
      terminationBy? := none
      partialFixpoint? := none
      decreasingBy? := none
      extraParams := 0
    }
  }]

[Cody Roux]

Yes! Thanks a bunch!