I am having an issue using Induct_on on a Hol_reln called Gm.
If I try to use it on a trivial goal it works, e.g.
> g `!Γ A. Gm Γ A ==> Gm Γ A`;
…
> e (Induct_on `Gm`);
OK..
1 subgoal:
val it =
(∀A. Gm {|A|} A) ∧ …
but if I use on a useful goal such as:
g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ) A`;
…
e (Induct_on `Gm`);
OK..
Exception raised at BasicProvers.Induct_on:
at BasicProvers.induct_on_type:
Type: :(α formula -> num) -> α formula -> bool is not registered in the types
database
Any ideas where I’m going wrong? Is the latter the goal in the wrong form?
Where should I look to figure this out?
Thank you,
Alex
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
