Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to make Eisbach's match functionality avai...


view this post on Zulip Email Gateway (Oct 04 2020 at 17:48):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I would like to understand if there is a simple methodology that would
enable one to transform Eisbach's method match into a tactic that can be
used as part of another tactic in Isabelle/ML? It does not seem that the
public interface of MATCH_METHOD allows for this at the moment. However, it
is interesting to note that the signature of MATCH_METHOD contains the
following comment: "FIXME proper ML interface for the main thing".

What would be the easiest workaround for this problem? On the other hand,
if a solution does not exist (apart from copy-pasting parts of the
implementation), would it be too much to ask to convert my query into a
feature request?

Kind Regards,
Mikhail Chekhov

view this post on Zulip Email Gateway (Oct 05 2020 at 22:42):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I would like to provide a brief remark with regard to my last question on
the mailing list: "How to make Eisbach's match functionality available from
Isabelle/ML?". While I am still genuinely interested in finding an answer
to the question, it seems that it will no longer have a significant impact
on my work and, therefore, finding an answer has a very low priority for
me. Generally, you can view this email as a retraction of the question.

Kind Regards,
Mikhail Chekhov


Last updated: Dec 05 2021 at 23:19 UTC