Email Gateway (Aug 19 2022 at 13:07): Email Gateway (Aug 19 2022 at 13:07):From: li yongjian <lyj238@gmail.com>
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
Email Gateway (Aug 19 2022 at 13:07):From: li yongjian <lyj238@gmail.com>
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
Email Gateway (Aug 19 2022 at 13:07):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Email Gateway (Aug 19 2022 at 13:07):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 13:08):From: li yongjian <lyj238@gmail.com>
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.
Last updated: Apr 25 2024 at 08:20 UTC