recall for inductive type

Stream: Is there code for X?

[Asei Inoue]

Sometimes I want to quote a definition of an inductive type that has already been defined, but if I separate it with namespace, I cannot guarantee that it is equal to the source of the quote. Is there a way to cite the definitions as in recall, making sure they match?

import Mathlib.Tactic

def hoge := "hello"

recall hoge := "hello"

/-- error: constant 'Nat' has no defined value -/
#guard_msgs in
recall Nat := sorry

[Kim Morrison]

Not really. It's not impossible that one could implement a recall inductive Nat by modifying the name, compiling the inductive, and then checking that everything generated matches, but it seems a lot of work for a niche use case.