Re: [isabelle] abbreviated the MPair



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.