Hi Dylan,
I'm not aware of such a "tactical". In fact, I'm uncertain what you are
looking for. A tactical is a SML function used to build tactics. An
example is "REPEAT". It is of type "tactic -> tactic". Given a tactic,
it returns another tactic that applies the argument tactic repeatedly.
I
Thank you!
> On Jul 6, 2018, at 1:04 PM, Mario Xerxes Castelán Castro
> wrote:
>
> This is eta conversion. It is handled in HOL4 by the simplifier and both
> HOL4 and HOL Light have conversions called “ETA_CONV” that are more low
> level.
>
> On 06/07/18 12:01, Dylan Melville wrote:
>> Is
This is eta conversion. It is handled in HOL4 by the simplifier and both
HOL4 and HOL Light have conversions called “ETA_CONV” that are more low
level.
On 06/07/18 12:01, Dylan Melville wrote:
> Is there a tactical that shows that a term is equal to the same term with an
> added abstraction, for
Is there a tactical that shows that a term is equal to the same term with an
added abstraction, for example:
|- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n
Or even more simply
|- f:(num->bool) <=> (\x:num. f:(num->bool) )
