[isabelle-dev] Constructing types from strings

[Makarius]

On Fri, 13 May 2011, munddr at gmail.com wrote:

> Is there a way to create a type out of a string? I know there's the 
> antiquotation @{type...}, but if the string was stored as a value, eg, 
> val str = "nat => nat", @{type str} doesn't seem to work.

Maybe you mean Syntax.read_typ, although your description sounds quite 
differently.  These parse/check/read operations internalized 
specifications given in end-user syntax, so you don't "store" such 
strings.


 	Makarius