Hi Dylan,
1. Your "EX" is basically the same as listTheory.EXISTS_DEF (in HOL4). If
you are in HOL Light, I am sure there is an analogous definition already
available. You should use it, since there are lots of theorems proved about
it already and you will save on work.
2. The problem is likely
> show_types := true;
val it = (): unit
> INFINITY_AX;
val it = ⊢ ∃(f :ind -> ind). ONE_ONE f ∧ ¬ONTO f: thm
> Il giorno 23 lug 2018, alle ore 18:22, Dylan Melville
> ha scritto:
>
> Is there a way to print theorems with types displayed?
>
>> On Jul 23, 2018, at 12:20 PM, Thomas Tuerk wrote:
Is there a way to print theorems with types displayed?
> On Jul 23, 2018, at 12:20 PM, Thomas Tuerk wrote:
>
> Hi,
>
> hard to say, why it does not work without further details. However, one guess
> is that types do not match. I would recommend showing the types when printing
> the theorem.
Hi,
hard to say, why it does not work without further details. However, one
guess is that types do not match. I would recommend showing the types
when printing the theorem. I expect that P might be of type `'a ->
bool`. In this case you need to instantiate 'a to string first.
Best
Thomas
On
I have a theorem called EX which returns true when a value is an element of a
list. It is defined as:
thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t)
I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t` being a
long list of strings which contains “T”.
