coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mandy Martino <tesleft AT hotmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] how to prove and evaluate new function definition with this axioms
- Date: Sun, 7 Feb 2016 06:46:53 +0000
- Accept-language: en-US, zh-HK
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT COL004-OMC2S13.hotmail.com
- Ironport-phdr: 9a23:lHxloxZdniSybU9ZG4NxOKH/LSx+4OfEezUN459isYplN5qZpcq6bnLW6fgltlLVR4KTs6sC0LqJ9fq8EjZdvN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcePKF8V2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtB7dfFXEtN30/zMztrxjKCwWVrDNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPGMTwQaF8fD2486ZtT1e8lCocMzM37EnXjdB1haNf5hmmokoskMbvfIiJOa8mLevmdtQASD8ZUw==
Hi ,
Require Import Arith.
Parameter G : Type.
Axiom reflexive : forall x y z:G, x <= x.
Axiom symmetric : forall x y z:G, x = y <= y = x.
Axiom transitive : forall x y z:G, (z = y) * z <= (z = x) * x.
Regards,
Martin
- [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Pierre Casteran, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/09/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, John Wiegley, 02/09/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/09/2016
Archive powered by MHonArc 2.6.18.