CODEWITHSUNDEEP
coq
Alex Coleman
Alex Coleman

Reputation: 647

While it is expected to have type "forall..." in Coq

Basically, I want to do pose (h st) on this equation:

h : (forall st : state, (P st -> wp st) /\ sd st) ->
    forall st st' : state,
    extract d1 / st \\ st' -> P st -> Q st'

However, when I run the command, coq tells me:

The term "st" has type "state" while it is expected to have type
 "forall st : state, (P st -> wp st) /\ sd st".

What is the right step?

Upvotes: 0

Views: 119

Answers (1)

Jasper Hugunin
Jasper Hugunin

Reputation: 496

The problem is that st is the second argument of h, while the first is expected to have that complicated type in the error. You can instead do pose (fun H => h H st).

Upvotes: 1

Related Questions