Re: [isabelle] [isabelle-dev] Syntax.read_term ctxt



thank you for looking at my question!
but as far as i can see there seems to be a misunderstanding (#####################)
so i kindly ask once more:

---- Makarius <makarius at sketis.net> wrote:
On Thu, 3 Mar 2011, bonzai at inode.at 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 ts => @{term "x::int"}::ts);
#############################------######
> 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") $
###########################################################################-----####
(we would like to have Int.int here
##################################################################################
        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
[...]
   * 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

Thank you very much for any help,
  Mathias Lehnfeld






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