Re: [isabelle] Variables in locale assumptions

On 24/02/14 23:05, Makarius wrote:
The 'constrains' element is easier to get rid of.  I would like to see some constructive
proofs where you "need to constrain types", as you say. This is usually just a workaround
to specify locale type arguments, but if that would be supported directly, the need would
go away.
I know one use case where constrains is more convenient than parameter instantiation with for, namely to revert the renaming of type variables. I want type variables to have sensible names like 'state, not just 'a, 'b, 'c, 'd. Unfortunately, locale inheritance always renames them to 'a, 'b, 'c, etc., so I rename them back. Of course, this can be done with a for clause, too. But a for clause drops the mixfix syntax associated with the parameter, so would have to redeclare it; with constrains, I need not. And for consistency reasons, I prefer not to redeclare notation if it's not necessary. And if locale inheritance did not rename type variables, I'd not need constrains at all and be much happier.


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