Re: [isabelle] Proof_Context abstraction



Dear List,

Am Mittwoch, den 30.07.2014, 09:23 +0200 schrieb Lars Hupel:
> > 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.
> 
> This is going to sound very low-tech, but I usually copy-paste
> significant chunks or even a whole file into a "ML{* *}" block in a
> theory. This usually works fine and gives you the full markup.

great idea! I could copy the whole of proof_context.ML into a Scratch
file and Isabelle/jEdit helpfully gives me all the types of the internal
value. (Unfortunately I cannot make Isabelle use that copied
Proof_Context ;-))


Am Mittwoch, den 30.07.2014, 09:47 +0200 schrieb Peter Lammich:
> 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.

Thanks for that suggestion. Unfortunately, that does not help with code
that doesn’t have type signatures.

Greetings,
Joachim



-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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