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 ...
sorry

end

Andreas

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.

	Florian

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







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