Re: [isabelle] type_synonym



Am 12/08/2012 22:03, schrieb Makarius:
> On Sat, 11 Aug 2012, Tobias Nipkow wrote:
> 
>> surely one could also wrap that code up into a top level command?
> 
> I would rather make it a variant of the existing 'typ' command like this:
> 
>   typ T  -- "as before"
>   typ T :: S  -- "with sort check"

Great minds think alike ;-)
I hadn't suggested it myself because I thought you might object that this gives
the impression that "T :: S" is legal syntax for types in general.
But I am all for it!

Tobias

> I'll study the situation of the sources soon ...
> 
> 
>     Makarius





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