coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marko Malikovi� <marko AT ffri.hr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Automatic finding false hypothesis
- Date: Sat, 24 Nov 2007 16:42:25 +0100 (CET)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Greetings,
is there some another tactic (except "omega") which can automatically find
false hypothesis in form of inequality and solve the goal, for example:
Hyp1 : 5>6
I know just ident of hypothesis ("Hyp1") but not his statement (we don't
know is it 5>6 or 100<=50). So, "absurd" tactic is not enough.
If it is just a "omega" tactic, can somebody explain me this error:
User error: Omega: Unrecognized atomic proposition: my_proposition
Thank you very much,
Marko Malikoviæ
- [Coq-Club] Automatic finding false hypothesis, Marko Malikoviæ
- Re: [Coq-Club] Automatic finding false hypothesis, Sean Wilson
- Re: [Coq-Club] Automatic finding false hypothesis,
Edsko de Vries
- Re: [Coq-Club] Automatic finding false hypothesis,
Marko Malikoviæ
- Re: [Coq-Club] Automatic finding false hypothesis, Sean Wilson
- Re: [Coq-Club] Automatic finding false hypothesis,
Marko Malikoviæ
Archive powered by MhonArc 2.6.16.