Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] abbreviated the MPair

Email Gateway (Aug 18 2022 at 19:45):

From: Abdullah <mr.ab15@gmail.com>
Dear All

I would to do that:

the notation {X ,Y} abbreviates MPair X Y

which I have define MPiar as type of message as follow

datatype message =
MPair message message.

what is the best way to do it. I have tried to do it by translations but is
not work as

datatype message =
MPair message message.

translations
"{X,Y}" <=> "MPair X Y"

Best Regards,

Email Gateway (Aug 18 2022 at 19:45):

From: Johannes Hölzl <hoelzl@in.tum.de>
Am Freitag, den 18.05.2012, 10:58 +0100 schrieb Abdullah:

Dear All

I would to do that:

the notation {X ,Y} abbreviates MPair X Y

In Isabelle/HOL {X, Y} is the set consisting of the elements X and Y,
you need to use another syntax lie {| X, Y |}.

which I have define MPiar as type of message as follow

datatype message =
MPair message message.

You are missing a base case for "message"! This definition fails at the
non-emptiness check.

The datatype command already allows you to define the syntax, like:

datatype msg = Pair msg msg ("{| _, _ |}")
| Node

term "{| Node, {| Node, Node |} |}"

Regards,

• Johannes

what is the best way to
do it. I have tried to do it by translations but is
not work as

datatype message =
MPair message message.

translations
"{X,Y}" <=> "MPair X Y"

Best Regards,

Greetings,
Johannes

Last updated: Apr 18 2024 at 04:17 UTC