Email Gateway (Aug 22 2022 at 17:35): 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
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"
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.
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: Nov 21 2024 at 12:39 UTC