The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Omer --

This line will do it for you:

Arguments fin_to_nat !n !f /.

It is using the customization to simpl features added in 8.4pl4. They are documented here: http://coq.inria.fr/coq/refman/Reference-Manual010.html#hevea_tactic135

On Thu, Sep 25, 2014 at 4:48 AM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

I have these two definitions: http://lpaste.net/111596 . If you try to
run this program, you'll realize that in line 13 the term is not
simplified, while in line 14 it's simplified to "3". Is it possible to
make first definition working with simpl, without giving away tactics?

Thanks..

---
Ömer Sinan Ağacan
http://osa1.net

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/