Re: [isabelle] Conversion for translation into combinatory logic?

Hi Florian,

Am 02.10.2014 um 17:59 schrieb Florian Haftmann <florian.haftmann at>:

> 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.


ML {*
Meson_Clausify.introduce_combinators_in_cterm @{cterm "%x::'a. Suc 0"}


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