Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] goal selectors; tactic expressions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] goal selectors; tactic expressions


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] goal selectors; tactic expressions
  • Date: Fri, 25 Jan 2019 05:54:46 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:FfAzfx39nTiNpsWHsmDT+DRfVm0co7zxezQtwd8ZseIRKvad9pjvdHbS+e9qxAeQG9mDu7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUoBO9qBJwzIHZe52VO+Fkc6/BYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+lGtYnyuV4OrBujDgeiHuzuxCRIhnjw3aYn1OkvFR/J3BY+ENILsHXYttv7O70cUOCuy6nIyy7OYOlQ2Tfg8oTHbA0uoeyWUb1qbMrc0E8iHB7GgFWIsYHoMC+Z2v4Qv2SH7edsT/+jhmAlpg1rpjWj2t8gh4bNi44P11zJ8SV0zJwoKdGmVEJ3e8OoHZVTui2COYt5XMAvT31ttSs/zrALuoW0cScPxZg6yRPQdeGIfo2G4h39V+udPTJ1iGx+d7KxiBu/91WrxPfmWcmuyllKqzJIktnSuXAJ0Bze8tSKRfVg8Eu9xDqDzh3d5eNKLEwtkqrUMIAuzqQ3lpoOrUTMBSj2mFjwjKCLbEkk4vKo6+P7Yrr4upCcK450igb4Mqg0ncy/HPg4MgwJX2ic+uSwzqHs/Ur8QLlSj/02lLfWsIzCKMkUuqK1GRJZ3poh5hqlEjur3tYVkWMDIV5ZYB6HipLmO1DKIPD2F/e/hFGsnS9vyf/YJL3uHJDNL3jZnLnvZ7l85VVcyA01zd1E/Z1UDKwBLOjtVUDsqdzUFAU2MxGsz+b9FNp9zp8eWX6IAqKBLKzStkaI6vszLOmIeY8aoy3wK+Ml5v7rlX82g0URfaiv3ZsNaXC3BO5qI0uDYSmkvtBUW2wNp081SPHgoFyESz9aIXioFepo7TYiTYmiEI3rR4a3gbXH0j3tTbNMYWUTKF2WHHL5P6mNROwLbmrGAMJ7nzkVE5SoVJQm0zmnshK8xrZ6aOPJrH5L/an/3cR4srWA3So58iZ5WpzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPIqivpFU9Ff+rVAT1VjbMKO/6lBE9n3Hzn5UJKRUl//GIevByx3Q94shdYTMR4kRoeSyyvb1i/vOIc70ryGAJtorfD14kOpfoNG+i2D06MsyV47XsFIKGuqwLZl8BTeDJLIlEPfkLu2caMb32jG82LRlGc=

Hi Cyprian,

What I wanted is what I would express as
repeat (all : solve_eqs)
but it seems as though that form is forbidden.

The various things I tried as indicated in my earlier email were simply
looking for alternatives that work.

Detailed background to what I want: solve_eqs doesn't seem to enlarge
the number of goals in the cases where I want to use it, and sometimes
solves a goal, sometimes only after solve_eqs has instantiated an evar
in another goal, sometimes only after being repeatedly called on the
same goal (where each time it simplifies the goal)

Cheers,

Jeremy


On 01/25/2019 10:00 AM, Cyprien Mangin wrote:
> What you probably meant is something like "all : repeat solve_eqs"

Archive powered by MHonArc 2.6.18.

Top of Page