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 28/07/20 a las 4:35, Manuel Eberl escribió:
> Well, if you want to do it the "proper" way, you need a logic with an
> explicit notion of undefinedness.
In HOL4 one can use the option types.
___
hol-info mailing list
hol-info@lists.sourceforge.net
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
