[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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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