The Coq mailing list

[GANGCHEN5 AT aol.com]

I find that the Decompeq tactic written by Pierre Courtieu can solve my problem.
Decompeq is a useful tool for proving equalties. Thanks to Pierre.


My previous message is due to a mistake of my own. I defined a function g with an implicit argument, so the total number of its arguments is 4 instead of 3. My tactic only deals with functions with less than 4 arguments, so it failed. The first time I tried Decompeq by cutting off the part dealing with 4 or more arguments, so it did not work. It would be desirable if there were methods to define tactic to handle arbitrary arguments.


Gang