Re: [isabelle] A type unification error



Hi Yongjian,

Although the reference is vague, I assume this is also about 
the programming cookbook and the code in question is:

ML{*
val (pform, table) =
       Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or>  B"} Termtab.empty;

SatSolver.invoke_solver "dpll" pform
*}

Note that the code in your theory *differs* from the above by
first including the file prop_logic.ML.

ML{*
use "/usr/local/Isabelle2011/src/HOL/Tools/prop_logic.ML";
val (pform, table) =
       (Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or>  B"} Termtab.empty);
pform;

SatSolver.invoke_solver "dpll" pform;
*}

If you remove this line, your code works. I guess the problem has 
something to do with redefining types in ML, which would explain
the puzzling error message.

BTW, a more robust way to reference files would be

  use "~~/src/HOL/Tools/prop_logic.ML"

Hope this helps,
Christian 

On Monday, June 18, 2012 at 06:13:04 (+0100), li yongjian wrote:
 > Dear all:
 > 
 > I'm trying your tutorial material on SAT  solver (page 196).
 > 
 >    I meet a type error that I cannot solve. Could you please do me
 >    a hand?
 >    see line 64 in the attachment.
 > 
 > The error says that Isabelle cannot unify the same type .
 > 
 >    regards!
 > xmachineLearning.thy, machineLearnin [Press RETURN to save to a file]

-- 





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