coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Durjay Chowdhury <durjaycsecu AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Applying Lemma in fold_left
- Date: Mon, 15 Aug 2016 00:20:18 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=durjaycsecu AT gmail.com; spf=Pass smtp.mailfrom=durjaycsecu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f177.google.com
- Ironport-phdr: 9a23:LFU3BB08qhitDHjMsmDT+DRfVm0co7zxezQtwd8ZsegQK/ad9pjvdHbS+e9qxAeQG96KsrQd16GP6vioGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMR2HHkOOs6bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4BLEVE6E4mYWemQQiBtBRQbfvz/gWZKknjbgtONskAKaOtL6Ta0uSHz247pxShb5gzwKPCMR/2Tei8g2h6Ve9kHy7ydjypLZNdnGfMF1ebnQKIsX
Hlw,
I am new in Coq. I am stack in a prove related to fold_left. I already proved a lemma: Lemma fold_left_zero {a : Type}: forall (l : list a) (n : nat), fold_left (fun (n1 : nat) (_ : a) => n1) l n = n.
fold_left
(fun (n : nat) (_ : x) =>
fold_left (fun (n0 : nat) (_ : y) => n0) elements n)
elements 0 = 0
- [Coq-Club] Applying Lemma in fold_left, Durjay Chowdhury, 08/15/2016
- Re: [Coq-Club] Applying Lemma in fold_left, Laurent Thery, 08/21/2016
- RE: [Coq-Club] Applying Lemma in fold_left, Soegtrop, Michael, 08/21/2016
- Re: [Coq-Club] Applying Lemma in fold_left, John Wiegley, 08/21/2016
Archive powered by MHonArc 2.6.18.