The Coq mailing list

[���� <hskiowa AT kaist.ac.kr>]

Dear coq-club,

 

I an wondering how to automate searching process using Ltac.

Can I code a tactic to do searching for past-established theorems, instead of manually doing SearchAbouts.

I thought "Hint Resolve" and "auto with ..." did the similar job, but they don't seem powerful enough in that I cannot put in keywords to narrow down my choices.

 

I am thinking of buliding a weak ATP out of Coq.

Do people think it feasible?

 

HyungSun Kim