Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] parsing a goal


view this post on Zulip Email Gateway (Aug 22 2022 at 17:35):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
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
Scratch.thy

view this post on Zulip Email Gateway (Aug 22 2022 at 17:35):

From: Peter Lammich <lammich@in.tum.de>
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"

view this post on Zulip Email Gateway (Aug 22 2022 at 17:36):

From: Dominique Unruh <unruh@ut.ee>
In addition to Peter's insight:
To get the same parsing behaviour in both cases, use Syntax.read_prop in
the ML code.
This will give you the same error in ML as in the lemma command.
(And Peter's fix works there, too.)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Aug 22 2022 at 17:37):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Peter and Dominique,

Thanks for your help!

Cheers,

Jeremy


Last updated: Mar 29 2024 at 04:18 UTC