Skip to Content.
Sympa Menu

coq-club - [Coq-Club] any ways to make this definition working with [simpl] ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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

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



Archive powered by MHonArc 2.6.18.

Top of Page