Match on Expr in delaborator

Stream: metaprogramming / tactics

[discuss9128]

Is there a better way to match on Exprs? I just want to get the Nat out, but there's all this invisible implicit stuff in the way.

import Lean
open Lean PrettyPrinter Delaborator SubExpr

inductive term
  | var : Nat → term

@[delab app.term.var]
def delab_term_var : Delab := do
  let e ← getExpr
  dbg_trace f!"expr {e}"
  let _ ← withAppArg do
    let idxExpr ← getExpr
      let index : Nat ← match idxExpr with
        | .app (.app (.app (.const ``OfNat.ofNat _) _) (.lit (.natVal n))) _ =>
          dbg_trace f!"matched {n}"
        | _ =>
          dbg_trace f!"did not match"
  failure

#check (term.var 0)

-- prints
-- expr term.var (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
-- matched 0

[Mirek Olšák]

You might want Lean.Expr.nat?

open Qq in
run_meta
  let e : Q(Nat) := q(5)
  match e.nat? with
  | none => logInfo "no match"
  | some n => logInfo m!"matched {n}"

[František Silváši 🦉]

For a more general approach, have a look at the quote library.

[discuss9128]

.nat? was what I was looking for, thank you! The library is very interesting too and I'll try it out.