Re: [isabelle] string -> const
On Mon, 13 Feb 2006, Sean McLaughlin wrote:
> Is there a way to go from a string to a const without incurring error
> messages? EG. Right now I have:
> fun type_of_const c = type_of (read c) handle _ => type_of (read ("op " ^ c))
Just note that handling *any* exception with a "_" pattern is a bad idea.
This would also cover Interrupt raised by user interaction, which is not
what you want here. The above can be made to work using
Output.transform_error, but it is easier to avoid user-level functions
like "read" in the first place.
Just use Sign.const_type, maybe after Sign.intern_const if name space
lookup should be included as well.
This archive was generated by a fusion of
Pipermail (Mailman edition) and