Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] short-cut for defining inductive relations

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: Lawrence Paulson <lp15@cam.ac.uk>
No fundamental reason that I can think of. Somebody simply has to
find the energy to do this...

Larry

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: Makarius <makarius@sketis.net>
This is not as easy as it looks on the surface. Nevertheless there are
plans the re-implement the concept of inductive predicates in a more
advanced manner (within a locale context etc.); this will also do away
with the syntax/translations incantations.

Makarius

Last updated: May 03 2024 at 04:19 UTC