Suppose I have a theorem like “P x ⇒ f x = t” where t is a metavariable
for an expression to which “f x” should evaluate. Is it possible to have
computeLib attempt to evaluate “P x” to “T” and then use “f x = t” to
compute?
___
hol-info mailing list
hol
I think so, for example, if "x" is a concrete term, then EVAL "f x" should
return a theorem |- f x = c. However, if function f is only defined for x
meeting P, then things may be more fiddly.
Konrad.
On Thu, Jul 30, 2020 at 2:40 PM Mario Xerxes Castelán Castro <
marioxcc...@yandex.com> wrote:
>
El 30/07/20 a las 16:14, Konrad Slind escribió:
> I think so, for example, if "x" is a concrete term, then EVAL "f x"
> should return a theorem |- f x = c. However, if function f is only
> defined for x meeting P, then things may be more fiddly.
That is the case relevant at hand, where the equatio
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 c
