Re: [isabelle] How to check type information in Isabelle/ML



On 18.08.2014 19:10, Wenda Li wrote:
> Dear Isabelle experts,
>
> I was wondering if there is an easy way to jump to the file where a
> type in Isabelle/ML is defined. For example, from
>
>   ML {*
>   Object_Logic.atomize
>   *}
>
> we can know that the function Object_Logic.atomize is of type
>
>   val it = fn: Proof.context -> conv
>
> we can also jump to the definition file of Object_Logic.atomize by
> CTRL+left click at the method name. However, what if I want to know
> more about the type "conv", is there a quick way to jump to the file
> where "conv" is declared or defined? An ideal way might be to
> CTRL+left click at "conv", but it does not seem to work for now.
Such a feature would be nice (as well as the option to jump into a
structure, even if I don't know any exported function in the structure);
but to my knowledge, your best bet are the usual search features.

  -- Lars




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