I am trying to use SerAPI to parse tactics and find useful information from the S-expressions.
I notice if I parse
split, I will get the following sentence in S-expresssion:
(((v (Ser_Qualid (DirPath ()) (Id split)))
This line seems indicates
split is denoted by
However, when I parse
intro. I get the following result:
((Kername (MPfile (DirPath ((Id Notations) (Id Init) (Id Coq)))) (DirPath ()) (Id intro_#_4C69D577))
destruct H, I get:
(TacInductionDestruct false false
The resulted S-expressions show those tactics are not denoted by
What is the difference between the tactic denoted by
qualid in S-expression and those not denoted by
I am trying to find more tactics denoted by
quliad in Serapi, but I still have not find another.