I’ve been writing recursive functions over syntax trees a lot recently. I also like my Lean code to be concise, but as things start piling up, this becomes harder and harder. Take the following function over propositional logic formulas as an example:

inductive Formula where
| atom : String → Formula
| neg : Formula → Formula
| conj : Formula → Formula → Formula

def depth : Formula → Nat
| .atom _ => 1
| .neg c => 1 + depth c
| .conj c d => 1 + max (depth c) (depth d)

depth is recursive and depth is used three times in its own definition. This is fine for small functions, but it can become cumbersome for larger ones. This is an actual function over description logic syntax from a codebase im working on. (You don’t need to understand the details to see thats A LOT of polarize all all just to handle a pretty simple recursive traversal)

def polarize {σ : Signature} : 𝒞 σ → Side → 𝒞 σᵂᴷ
| ⊤, +ₚ => ⊤
| ⊤, -ₚ => ⊥
| ⊥, +ₚ => ⊥
| ⊥, -ₚ => ⊤
| [a]ₐ, side => [(a, side)]ₐ
| ¬ₜ c, +ₚ => polarize c -ₚ
| ¬ₜ c, -ₚ => polarize c +ₚ
| c ⊓ₜ d, +ₚ => polarize c +ₚ ⊓ₜ polarize d +ₚ
| c ⊓ₜ d, -ₚ => polarize c -ₚ ⊔ₜ polarize d -ₚ
| c ⊔ₜ d, +ₚ => polarize c +ₚ ⊔ₜ polarize d +ₚ
| c ⊔ₜ d, -ₚ => polarize c -ₚ ⊓ₜ polarize d -ₚ
| ∃[r] c, +ₚ => ∃[r] polarize c +ₚ
| ∃[r] c, -ₚ => ∀[r] polarize c -ₚ
| ∀[r] c, +ₚ => ∀[r] polarize c +ₚ
| ∀[r] c, -ₚ => ∃[r] polarize c -ₚ

In Dyalog APL, the symbol ∇ refers to the current function. I wanted something similar for Lean:

def∇ depth : Formula → Nat
| .atom _ => 1
| .neg c => 1 + ∇ c
| .conj c d => 1 + max (∇ c) (∇ d)

Lean doesn’t have this built in, but as usual, its macro system is powerful enough to implement it.

The macro Link to heading

import Lean

macro "∇" : term => do
  return Lean.mkIdent `«∇»

namespace SelfRec
open Lean Parser

@[command_parser] def defDel := leading_parser
  Command.declModifiers false >>
  "def∇" >> Command.declId >>
  ppIndent (many (ppSpace >> Term.bracketedBinder) >> Term.typeSpec) >>
  Term.matchAlts
end SelfRec

macro_rules
  | `(command| $mods:declModifiers def∇ $name:ident
      $binders:bracketedBinder* : $ty:term $alts:matchAlts) => do
      let del := Lean.mkIdent `«∇»
      `(command| $mods:declModifiers def $name
          $binders:bracketedBinder* : $ty := $del:ident
        where
          $del:ident : $ty
            $alts:matchAlts)

def∇ expands into an ordinary def whose body is a recursive where helper named «∇». For example our above depth function expands to:

def depth : Formula → Nat := «∇»
where
  «∇» : Formula → Nat
  | .atom _ => 1
  | .neg c => 1 + «∇» c
  | .conj c d => 1 + max («∇» c) («∇» d)

The separate term macro turns each bare ∇ into a reference to that helper. Lean.mkIdent is deliberate here: the reference needs to find the local helper, whereas an ordinary quoted macro expansion would be hygienic and miss it. Lean still checks that the recursion terminates.

Some Examples Link to heading

-- Fibonacci function
def∇ fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => ∇ (n + 1) + ∇ n

-- Evaluation of propositional formulae under a given valuation
def∇ eval (valuation : String → Prop) : Formula → Prop
| .atom s => valuation s
| .neg φ => ¬∇ φ
| .conj φ ψ => ∇ φ ∧ ∇ ψ

You can check out the examples on the web runner here!