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 ?
- [Coq-Club] The term "pYX" has type "com" while it is expected to have type "Imp.com"., fengsheng, 12/30/2012
- Re: [Coq-Club] The term "pYX" has type "com" while it is expected to have type "Imp.com"., Pierre Casteran, 12/31/2012
Archive powered by MHonArc 2.6.18.