Open yutakang opened 4 years ago
Maybe it is better to check if the relevant constant is defined with inductive or fun.
inductive
fun
Maybe it is better to check if the relevant constant is defined with
inductive
orfun
.