Re: [isabelle] parsing a goal



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> 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.