coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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
- Re: [Coq-Club] any ways to make this definition working with [simpl] ?, Gregory Malecha, 09/25/2014
Archive powered by MHonArc 2.6.18.