Re: [isabelle] shorter syntax?

Hi Vadim,

> fixes a::"'val::{comm_ring_1} list"
> If there is a way to define shorter alias for this?

in short, nothing simple except to leave out the curly brackets:

  fixes a :: "'a :: comm_ring list"

You could do fancy things on one of the type parsing/printing layers,
but this is nothing I would recommend here.


> For example, before I was working with reals and I had
> type_synonym 'vec' for 'real list' and I would use:
> fixes a::"vec"
> Any way to do something similar here?
> Thanks!
> Sincerely,
> Vadim Zaliva
> --
> CMU ECE PhD student
> Mobile: +1(510)220-1060
> Skype: vzaliva


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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