Re: [isabelle] Proof_Context abstraction



On Mi, 2014-07-30 at 09:23 +0200, Lars Hupel wrote:
> > Since you mention type-driven: Do you know of a way of having the
> > system tell me the types of non-exported functions in existing ML
> > code in Pure/? The exported functions have their types visible in the
> > signature specification.

I'm even more low-tech: I have a console open in src/, and use 
  grep "val <fun-name>:" -r .
this usually matches the line in the signature that declares the type.

The same could be achieved with jedits (mouse-intensive) hypersearch
feature.

--
  Peter





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