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 equation is buried in an implication because the function is only partially defined. Is there a standard way to deal with this? _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
