Re: [isabelle] A problem on ML-like function programming



Thanks for
Yannick Duchêne's advice.

I meet this problem because I use FL to automatically generate some Isablle
theory files for some case study.


On Mon, Dec 30, 2013 at 2:58 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I simply don't see what this question has to do with Isabelle. This list
> is about Isabelle, not about functional programming (even in ML).
>
> Larry Paulson
>
>
> On 29 Dec 2013, at 17:14, Yannick Duchêne (Hibou57) <
> yannick_duchene at yahoo.fr> wrote:
>
> > As no experts answered so far, I will try my two cents, with apologizes
> for not giving more.
> >
> > Do you mean printing to a PDF document? If Yes, then did you try
> antiquotations like "@{term fn_name}" and the likes? It's documented in
> Isar-Ref §4.2 (printed page 63). If Not, may be the question lacks
> precisions to me or is just out of my capabilities.
> >
> > Le Sun, 29 Dec 2013 15:27:22 +0100, li yongjian <lyj238 at gmail.com> a
> écrit:
> >
> >> Dear experts:
> >>
> >>   Happy new year!
> >>
> >>  I have a question on analyzing the structure of a function in function
> >> language.
> >>
> >>  I use FL, a function language in with reflection feature.
> >>
> >>  My problem:
> >>
> >>  I have a simple function definition, and want to print its structure
> >>
> >>  let f x=x +1;
> >>
> >>  I want to print the value f as a string follows:
> >>
> >> " f x=x + 1";
> >>
> >> how to implement it? Of course, I want to generalize this to any
> function.
> >>
> >> regards!
> >> lyj
> >>
> >
> >
> > --
> > "Syntactic sugar causes cancer of the semi-colons." [1]
> > "Structured Programming supports the law of the excluded muddle." [1]
> > [1]: Epigrams on Programming -- Alan J. -- P. Yale University
> >
> >
>
>
>



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