Re: [Hol-info] EVAL when equations have an antecedent

2020-09-13 Thread Mario Xerxes Castelán Castro «Ksenia» 
El 31/07/20 a las 11:35, Mario Xerxes Castelán Castro «Ksenia» escribió:
> 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?

I made a pull request to add support of this case to computeLib:
<https://github.com/HOL-Theorem-Prover/HOL/pull/863>.



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Visualizing subgoals in a proof script

2020-08-09 Thread Mario Xerxes Castelán Castro «Ksenia» 
Thanks for the answers Michael, Freek, Mark.


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Visualizing subgoals in a proof script

2020-08-01 Thread Mario Xerxes Castelán Castro «Ksenia» 
Hello. In HOL4 is there a way to generate something like the entries in
Metamath proof explorer for the subgoals generated within a proof and
the tactics used to solve them? Example:



___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] EVAL when equations have an antecedent

2020-07-31 Thread Mario Xerxes Castelán Castro «Ksenia» 
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

Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem

2020-07-30 Thread Mario Xerxes Castelán Castro «Ksenia» 
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