Ssreflect Users Discussion List

[Beta Ziliani <>]

Hi Marcus,

I guess you're using the option Set Implicit Arguments, are you?  It
seems to me that P2Q has the first two arguments implicits.  You can
check this with "About P2Q".

Cheers,
B

On Thu, Apr 24, 2014 at 3:01 PM, Marcus Ramos
<> wrote:
> Hi,
>
> When I try to run the example of page 22 of the tutorial ("An introduction
> to small scale reflection in Coq") I get an error message and can´t
> understand why. See below:
>
> Section Page_22.
> Variables P Q: bool->Prop.
> Hypothesis P2Q: forall a b, P(a || b)-> Q a.
> Goal forall a, P (a || a) -> True.
> move => a HPa.
> (* error occurs in the next line *)
> move: {HPa}(P2Q _ _ HPa) => HQa.
>
> The error message (Proof General/Windows) is:
>
> Toplevel input, characters 12-19:
> Error: Illegal application (Non-functional construction):
> The expression "P2Q ?9" of type "Q ?7"
> cannot be applied to the term
>  "?11" : "?10"
>
> Any help appreciated. By the way, the next two examples work fine.
>
> Thanks,
> Marcus.
>
>