[isabelle] Conversion for translation into combinatory logic?

Hi all,

in HOL, is there any conversion turning a term t into an equivalent t'
with all abstractions turned into expressions of combinatory logic? E.g.

  comblogic_conv «%x. Suc 0» ~> «K (Suc 0)»

I dimly remember that metis and/or sledgehammer once used to have
something like this, and maybe it is still there somewhere.

The reason is that I collect some ideas how to implement a more robust
approach towards evaluation using code generation, and a preliminary is
that the terms to be evaluated are lambda-free.  Hence such a conversion
would make a convenient preprocessor.

Thanks a lot,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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