{motive : Mathlib.Meta.NormNum.NormNumExt → Sort u} →
  (t : Mathlib.Meta.NormNum.NormNumExt) →
    ((pre post : Bool) →
        (eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e)) →
          (name : Lean.Name) → motive { pre := pre, post := post, eval := eval, name := name }) →
      motive t