Re: [isabelle] shorter syntax?

Hi Vadim

Here's another thought on this. If it is just about avoiding the ubiquitous sort constraint for one specific type variable, you can fix the type variable locally in an anonymous context. Here's an example:

context fixes dummy :: "'val :: comm_ring_1" begin

lemma foo
  fixes a :: "'val"
  assumes ...
  shows ...



On 10/09/14 09:40, Florian Haftmann wrote:
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?


Vadim Zaliva

CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

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