coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] any ways to make this definition working with [simpl] ?

From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
To: coq club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] any ways to make this definition working with [simpl] ?
Date: Thu, 25 Sep 2014 15:42:31 +0300

2014-09-25 14:44 GMT+03:00 Gregory Malecha
<gmalecha AT cs.harvard.edu>:
> Arguments fin_to_nat !n !f /.

Amazing, it worked! That may solve a lot of problems I've been having
with tactics lately, I should read about this syntax sometime. Thanks!

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

[Coq-Club] any ways to make this definition working with [simpl] ?, Ömer Sinan Ağacan, 09/25/2014
- Re: [Coq-Club] any ways to make this definition working with [simpl] ?, Gregory Malecha, 09/25/2014
  - Re: [Coq-Club] any ways to make this definition working with [simpl] ?, Ömer Sinan Ağacan, 09/25/2014