Re: [Hol-info] EVAL when equations have an antecedent
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
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
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 https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] EVAL when equations have an antecedent
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
