function - 是否有一个内置函数可以获取数据类型条目的名称？

Question

我只想知道是否可以在 Isabelle 中获取数据类型条目的名称。例如：

datatype Test = A int | B string | C nat

是否有执行以下操作的函数（暂时调用它f）？

f(A 5) = A
f(B ''hi'') = B
f(C 234789623) = C

提前致谢！

标签： functionisabelle