Re: [Hol-info] EVAL when equations have an antecedent

[Mario X. C. C. «K. <mar...@ya...>]

El 31/07/20 a las 11:35, Mario Xerxes Castelán Castro «Ksenia» escribió:
> That is the case relevant at hand, where the equation is buried in an
> implication because the function is only partially defined. Is there a
> standard way to deal with this?

I made a pull request to add support of this case to computeLib:
<https://github.com/HOL-Theorem-Prover/HOL/pull/863>.