Ssreflect Users Discussion List

[Marcus Ramos <>]

Hi Maxime,

That works, thank you! However, I guess the text of the tutorial should then be corrected to:

move: (P2Q HPa) => HQa.

instead of:

move: (P2Q _ _ HPa) => HQa.

Best Regards,

Marcus.

2014-04-24 15:35 GMT+02:00 Maxime Dénès <>:

Hi Marcus,

I haven't looked at this example, but as Beta said, if you use implicit arguments, you should probably write:

move: {HPa}(P2Q HPa) => HQa.

Hope it helps!

Maxime.

On 04/24/2014 09:01 AM, 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.