Ssreflect Users Discussion List

[Marcus Ramos <>]

Hi Beta,

Yes I am, just as recommended in the tutorial:

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.

Require Import path choice fintype tuple finfun finset.

Set Implicit Arguments.

Unset Strict Implicit.

Import Prenex Implicits.

Still, it does not work.

Best Regards,

Marcus.

2014-04-24 15:08 GMT+02:00 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.
>
>