Re: [isabelle] parsing a goal



Hi Peter and Dominique,

Thanks for your help!

Cheers,

Jeremy

On 06/15/2018 05:13 PM, Dominique Unruh wrote:
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.


On 14 June 2018 at 18:40, Peter Lammich <lammich at in.tum.de <mailto:lammich at in.tum.de>> wrote:

    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.