coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] or in ltac tryif

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] or in ltac tryif
Date: Sun, 15 Dec 2019 08:16:48 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
Ironport-phdr: 9a23:pCbxCx1WLkIxl0E9smDT+DRfVm0co7zxezQtwd8ZseIWKfad9pjvdHbS+e9qxAeQG9mCsLQe07Gd4/+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalsIBmqowjducobjIl/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEtIb9p1oOrQC+BQayB+Pk1yNFhnns0q08zusqDAbL0xY7ENIOsXTUt9X1O7kRUeyv1qbIyy/Mb/VL1jvn6YjIcwwhof6XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGaV6OpgUPigi28hqwxpvjevwd0sio/XiYIRzlDI7zt2z5soJdC+VUV1YsakHYNOuy2GM4Z6WMAvTmFytCony7ALuIS3cScKxZkh2hXRceaIc5KS7RLmTOuRISl3hHZieL+ngha960mgyunlWsm111ZGszNJktfDu30NzRDT5c+HSvxy/kelxzmDzRzc6uZBIUwslKrbLYAuwqIom5YNrUjOGjX6lUb2gaOMa0kp++ml5/7ob7jmvpOcMpV7igD6MqQggMy/BuE4PxAUUGeA+eS81abj/U3nT7VJlPE5iK/Zv4rcJcsGvKK5Ag5V0pos6xukADem1c4XnXgDLF5fZB2HiI3pN0nUIP/kFfe/n0iskDBzyv/aOb3hG4zBIWTHkLf8Zrlw8FVcyQo2zdBH/Z1YELABIPTpWk/wrtPUFBE5Mxbni9rgXd56z8YVXX+FSvuSN7qXuluV7MouJfONbckbomCuBeIi4qvHh384gl8QfuGA25IRZDjsF/5mIl6ZbHmqi9EIF2tMvwsiQ8TljVSDVXhYYHPkDPF03S0yFI/zVdSLfYuqmrHUhH7mTK0TXXhPDxW3KVmtd4iAXK1ROiebI8skkztdELb9Fsku0hahsAK8wL1ifLKNq38o8Kn73d0w3NX90BQ79Dh6FcOYijjfQGR9n2dOTDgzjvkm/R5Nj2yb2K09uMR2UMRJ7qoQAAg/PJ/Yied9DoKqVw==

Is there a way in Ltac to denote the logical disjunction of the conditionals fed to tryif?

I have

tryif has_evar L
then fail
else
tryif has_evar R
then fail
else some_tac.

I wish I could write it as:

tryif (has_evar L or has_evar R)
then fail
else some_tac.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] or in ltac tryif, Abhishek Anand, 12/15/2019
- Re: [Coq-Club] or in ltac tryif, Jason Gross, 12/15/2019