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
This archive was generated by a fusion of
Pipermail (Mailman edition) and