Re: [isabelle] parsing a goal



The parser tries to parse as Boolean by default, wrapping around a
HOL.Trueprop automatically.

Use PROP to override.

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

note: This is the same as

lemma test: "A==>A"


--
  Peter


On Fr, 2018-06-15 at 00:57 +1000, Jeremy Dawson wrote:
> 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




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