Re: [isabelle] Same proof state, different metis behaviour




On Thursday, October 4, 2012 at 09:57:35 (+0100), Jasmin Blanchette wrote:
 > 
 > Could you specify precisely which version of Nominal2 and of Isabelle you're using? I'm using the latest of both and get this error from Nominal2:

Fixed now. Thanks for pointing this out.

Christian


 > 
 > *** Error (line 251 of "/Users/blanchet/misc/nominal2/Nominal/nominal_dt_alpha.ML"):
 > *** Type error in function application.
 > ***    Function: Inductive.add_inductive_i :
 > ***       inductive_flags ->
 > ***       ((binding * typ) * mixfix) list ->
 > ***       (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> inductive_result * local_theory
 > ***    Argument: {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = ..., ...} :
 > ***       {coind: bool,
 > ***        no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
 > ***    Reason:
 > ***    Can't unify {coind: bool, no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, skip_mono: bool, quiet_mode: bool}
 > ***       to {coind: bool,
 > ***           no_ind: bool, no_elim: bool, verbose: bool, alt_name: binding, fork_mono: bool, skip_mono: bool, quiet_mode: bool}
 > ***       (Different number of fields)
 > *** 
 > *** At command "use" (line 27 of "/Users/blanchet/misc/nominal2/Nominal/Nominal2.thy")
 > 
 > > Nevertheless, in the first lemma, metis finds the proof sufficiently
 > > fast, while in the second, it does not find any proof. As this is
 > > probably not the intended behavior I was told to report that here.
 > 
 > That certainly sounds strange. Are the goals really identical, or is one using metaequality and the other object-level equality?
 > 
 > Jasmin
 > 
 > 

-- 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.