coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Victor Porton <porton AT narod.ru>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Dependent records conditions
- Date: Mon, 21 Nov 2011 18:53:56 +0400
- Envelope-from: porton AT yandex.ru
Parameter A : Set.
Parameter B : A -> Prop.
Structure Foo := mkFoo { a : A; b : B a }.
(* How to prove this lemma? Is it possible at all? *)
Lemma my (u : Foo) : B (@a u).
--
Victor Porton - http://portonvictor.org
- [Coq-Club] Dependent records conditions, Victor Porton
- Re: [Coq-Club] Dependent records conditions,
Pierre Casteran
- Re: [Coq-Club] Dependent records conditions,
Daniel Schepler
- Re: [Coq-Club] Dependent records conditions, AUGER Cedric
- Re: [Coq-Club] Dependent records conditions,
Daniel Schepler
- Re: [Coq-Club] Dependent records conditions,
Pierre Casteran
Archive powered by MhonArc 2.6.16.