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: > 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-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
