Re: [isabelle] Program extraction, accessing instantiated proof terms



On 04/20/2015 03:07 PM, Matthias Schlaipfer wrote:
Hello,

I am trying to understand the implementation of program extraction in Isabelle. I am wondering whether it is possible to access the instantiated proof terms (like the output of the Isar commands prf or full_prf) in the extract/extr functions in Pure/Proof/extraction.ml.

I tried printing them for better understanding and thought it should be possible similar as in string_of_prfs (in Pure/Isar/isar_cmd.ML), but I don't know how to access the context, or if it is even possible at this point.

Hi Matthias,

you can print proof terms using Proof_Syntax.pretty_proof and Pretty.writeln. There is no
context available in the extract function, but you can turn the thy argument into a context
by applying Proof_Context.init_global.

Greetings,
Stefan




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