Skip to Content.
Sympa Menu

coq-club - [Coq-Club] The term "pYX" has type "com" while it is expected to have type "Imp.com".

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The term "pYX" has type "com" while it is expected to have type "Imp.com".


Chronological Thread 
  • From: "fengsheng" <fsheng1990 AT 163.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] The term "pYX" has type "com" while it is expected to have type "Imp.com".
  • Date: Sun, 30 Dec 2012 10:14:22 +0100 (CET)

Error:
In environment
H : forall st st' : state, pXY / st || st' <-> pYX / st || st'
st : state
Heqst : st = empty_state
st1 : state
Heqst1 : st1 = update (update empty_state X 0) Y 2
H1 : pYX / st || st1
st2 : state
Heqst2 : st2 = update (update empty_state Y 0) X 0
H2 : pYX / st || st2
The term "pYX" has type "com" while it is expected to have type "Imp.com".

When I try to proof that st1 = st2, it just didnt do that and give the error
information above. What does that mean and how to solve it ?



Archive powered by MHonArc 2.6.18.

Top of Page