Email Gateway (Aug 19 2022 at 16:32): Email Gateway (Aug 19 2022 at 16:32):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
is there a deeper reason why thin_tac allows schematics in the pattern,
but no underscores?
Email Gateway (Aug 19 2022 at 16:47):From: Makarius <makarius@sketis.net>
thin_tac belongs to the res_inst_tac family, which has the following
comment in the ML sources: (* FIXME cleanup this mess!!! *) -- it means
that this is highly non-canonical within Isar, and dummy patterns via
underscore belong to certain Isar syntax policies that are not observed
here.
After so many years of these remaining oddities in the sources, there is
actually a perspective to overcome it all, and have proof methods with a
goal focus that fit into Isar conceptually -- as part of the Eisbach work.
Makarius
http://stop-ttip.org 980,792 people so far
Last updated: Apr 20 2024 at 01:05 UTC