coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] cleaning up after 'field'

From: Michael Shulman <shulman AT sandiego.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] cleaning up after 'field'
Date: Thu, 5 Nov 2015 08:59:17 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f172.google.com
Ironport-phdr: 9a23:MaaJcxZ2jtA2IS8FzG+ZBDr/LSx+4OfEezUN459isYplN5qZpcu4bnLW6fgltlLVR4KTs6sC0LqL9fu9Ejdcqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh730oMCYOFkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6k4WJUeWELmFIcCA/cqRr+Q53Zsy3gt+M71jPMbuPsSrVhfDWp765mTFfTiDoDMjc/uDXMitF0iatdiAmooRB+zoHTJoyZKawtLevmYdoGSD8ZDY5qXCtbD9b5NtNXAg==

Is there a standard tactic that can automatically solve the non-zero
conditions left over by "field", at least in simple cases? E.g. if
the condition is "x - 1 != 0" and we have "x != 1" as a hypothesis?

[Coq-Club] cleaning up after 'field', Michael Shulman, 11/05/2015
- Re: [Coq-Club] cleaning up after 'field', Frédéric Besson, 11/05/2015
- Message not available
  - Re: [Coq-Club] cleaning up after 'field', Michael Shulman, 11/05/2015