This is a situation where type abbreviations probably won't
help you, since you have to mention all the type variables
when writing the abbreviation (just like in ML).
Antiquotations might help. At the ML level you could write
val my_type = ``:('a,'b,'c,'d,'e,'f,'g,'h)my_type``
and then later in a type quotation you could write
``: .... ^my_type ... ``
and in a term quotation you could write
`` ... (r : ^(ty_antiq my_type)) ... ``
for example.
Konrad.
Bingham, Jesse D wrote:
> I've defined a nested record type structure my_type that contains 8
> type variables 'typevar1,...,'typevar8. Whenever I mention this
> type, I have to do something like
>
> ('typevar1,'typevar2,'typevar3,'typevar4,'typevar5,'typevar6,'typevar7,'typevar8)my_type
>
> which is obviously a little messy. My question (and I'm not sure if
> this even makes sense): is there a way to make type variables have
> scope as being a whole theory? I suppose what I'm after is the
> ability to simply write
>
> my_type
>
> or something slimilar and have HOL interpret this as the messy type
> expression above. Thanks
>
> -Jesse
> ------------------------------------------------------------------------
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems? Stop.
> Now Search log events and configuration files using AJAX and a browser.
> Download your FREE copy of Splunk now >> http://get.splunk.com/
> ------------------------------------------------------------------------
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems? Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
