Thanks for the bug report! I've put it into our issue tracker at https://github.com/mn200/HOL/issues/128
Michael
On 10/08/13 23:45, Rob Arthan wrote:
> I think the section on new_type_definition in the HOL 4 reference manual
> should
> say that it fails if the theorem in the parameter has free variables. E.g.,
>
> app load ["PairedLambda", "Q"]; open PairedLambda pairTheory;
> val tyax1 = new_type_definition ("bad1", Q.prove(`?p.(\(x,y). ~(x /\ y /\ z))
> p`,
> Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));
>
> correctly results in an error:
>
> Exception-
> HOL_ERR
> {message =
> "at Thm.prim_type_definition:\nsubset predicate must be a closed term",
> origin_function = "new_type_definition", origin_structure = "Definition"}
> raised
>
> In fact, this is the only error message I can provoke:
>
> val tyax2 = new_type_definition ("bad1", Q.prove(`?p.FST p \/ SND p`,
> Q.EXISTS_TAC `(T,T)` THEN REWRITE_TAC []));
>
> results in the same exception even though what is wrong here is that the
> theorem
> doesn't have the form |= ?x.t x
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite! It's a free troubleshooting tool designed for production. Get down to code-level detail for bottlenecks, with <2% overhead. Download for free and get started troubleshooting in minutes. http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
