elabPushTree — Mathlib

Lean4
@[command_elab pushTree, inherit_doc pushTree]
def elabPushTree : Elab.Command.CommandElab := fun stx => do
  Elab.Command.runTermElabM fun _ => do
      let head ← elabHead ⟨stx[1]⟩
      let thms := pushExt.getState (← getEnv)
      let mut logged := false
      for (key, trie) in thms.root do
        let matchesHead (k : DiscrTree.Key) : Bool :=
          match k, head with
          | .const c _, .const c' => c == c'
          | .other, .lambda => true
          | .arrow, .forall => true
          | _, _ => false
        if matchesHead key then
          logInfo m! "DiscrTree branch for {key }:{indentD (format trie)}"
          logged := true
      unless logged do
        logInfo m! "There are no `push` theorems for `{head.toString}`"
Похожие утверждения