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



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 “ at {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.