coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] why simpl does not work in this case?

From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
To: coq club <coq-club AT inria.fr>
Subject: [Coq-Club] why simpl does not work in this case?
Date: Mon, 3 Mar 2014 23:57:07 +0200

Hi all,

I have this term as goal: http://lpaste.net/100661 and it looks
solvable once I can simplify it by doing beta-reduction and then
simplifying `match n with ...` term(it will become `match 0 with` once
beta-reduction is done) ..

Any ideas why I can't simplify this term, and what should I do to simplify it?

Thanks..

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

[Coq-Club] why simpl does not work in this case?, Ömer Sinan Ağacan, 03/03/2014
- Re: [Coq-Club] why simpl does not work in this case?, Guillaume Melquiond, 03/03/2014