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
