David,
On 01/11/2019 16:13, David Topham wrote:
Ok, I can work within integers for awhile! I was trying to use the
general form of the geometric progression that may involve fractions,
but I can explore whole numbers more first. I see the "induction_thm"
won't work with R anyway since it has the base case as 0 and SML would
expect 0.0 there for domain R (at least that is what I am seeing so
far in trying to open_theory R and apply the thm).
I am trying wrk074 however open_theory "fincomb" fails so I need to
find out how to load that as pre-requisite.
The kind of induction embodied in induction_thm is good only for the
natural numbers ℕ, it does work for any other number system (not even
the integers, ℤ).
If you want to use the theories in maths_egs you have to download the
tar file from lemma-one.com and follow the instructions for installing it.
fincomb is provided by wrk073, but when you run the makefile all the
maths_egs theories will be built.
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
