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



Hi Florian,

Am 02.10.2014 um 17:59 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

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

Sure:

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

Jasmin





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