On Thu, 3 Mar 2011, [email protected] wrote:
i studied isabelle/isar implementation, isabelle/isar reference manual and the
isabelle cookbook.
what am i still doing wrong ?
structure Data = Proof_Data
(type T = term list
fun init _ = []);
val ctxt =
ProofContext.init_global @{theory} |>
Data.map (fn trms => @{term "x::int"}::trms);
Data.get ctxt;
Syntax.read_term ctxt "x + 1 = 2";
(* we get Free ("x", "'a") etc, but would expect ...
val it =
Const ("HOL.eq", "Int.int \<Rightarrow> Int.int \<Rightarrow>
HOL.bool") $
(Const ("Groups.plus_class.plus", "Int.int \<Rightarrow> Int.int
\<Rightarrow> Int.int") $
Free ("x", "Int.int") $ Const ("Groups.one_class.one", "Int.int")) $
(Const ("Int.number_class.number_of", "Int.int \<Rightarrow>
Int.int") $
(Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
(Const ("...", "Int.int \<Rightarrow> Int.int") $
Const ("Int.Pls...", "Int.int")))):
term
*)
I cannot reproduce the problem. This is the output of ML toplevel
declarations produced here:
structure Data : PROOF_DATA
val ctxt = <context>: Proof.context
val it = [Free ("x", "Int.int")]: Data.T
val it =
Const ("HOL.eq", "'a \<Rightarrow> 'a \<Rightarrow> HOL.bool") $
(Const ("Groups.plus_class.plus", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free
("x", "'a") $
Const ("Groups.one_class.one", "'a")) $
(Const ("Int.number_class.number_of", "Int.int \<Rightarrow> 'a") $
(Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
(Const ("...", "Int.int \<Rightarrow> Int.int") $ Const ("Int.Pls...",
"Int.int")))):
term
Further notes:
* trm, trms are a bad naming convention for terms; use t, ts or tm, tms
instead.
* You can ask questions about Isabelle/ML on the isabelle-users mailing
list. isabelle-dev means you are hooked on unofficial repository
versions for some reason, in which case you should also say which
one it is (e.g. via isabelle version -i).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
