[isabelle] parsing a goal




Hi,

In the file Scratch.thy (attached) the code

ML {*
val tm = Syntax.read_term @{context}
  "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))" ;
val ty = Term.type_of tm ;
*}

works fine, giving a term of type prop,
but the following code fails

lemma test: "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))"

with an error message which I don't understand:

Type unification failed: Clash of types "prop" and "bool"

Type error in application: incompatible operand type

Operator:  Trueprop :: bool \<Rightarrow> prop
Operand:   A \<Longrightarrow> A :: prop

Can anyone explain why this happens?

Thanks

Jeremy
theory Scratch imports Main begin
  
ML {*
val tm = Syntax.read_term @{context} 
  "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))" ;
val ty = Term.type_of tm ;
*}


lemma test: "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))"
(* error message is 
Type unification failed: Clash of types "prop" and "bool"

Type error in application: incompatible operand type

Operator:  Trueprop :: bool \<Rightarrow> prop
Operand:   A \<Longrightarrow> A :: prop
*)



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