Re: [isabelle] Proof_Context abstraction



Hello,


Am Dienstag, den 29.07.2014, 19:52 +0200 schrieb Makarius:
> > I’m trying to learn hacking Isabelle/ML
> 
> > Is there a way to mess with the internals of the Proof_Context directly, 
> > or would I have to change proof_context.ml for that (such as exposing 
> > map_data)?
> >
> > Or am I approach this task in a wrong way?
> 
> It depends whom you ask, and what you want to achieve.  Proper 
> understanding the systems needs long time of study, not quick hacking.  I 
> would go as far as to say that and "hacking" or "messing" is a not worth 
> the time spent on it.

there is always a first step, and different people learn in different
ways. I could have said “experimentation” if you like that word better.

I want to achieve sufficient knowledge of the Isabelle/ML layer to
implement a "unfold_in_context" command as outlined last week. I’d say
that learning to do that is worthwhile independent of whether such a
command is desirable.


So can I expect guidance from those on this list who already spent the
long time of study? Or is it expected for newcomers to study on their
own until they achieve mastery (or give up)?


Thanks,
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.