coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cuihtlauac ALVARADO <cuihtlauac.alvarado AT rd.francetelecom.fr>
- To: coq-club AT inria.fr
- Subject: let: 7 vs 6
- Date: Thu, 17 May 2001 15:23:24 +0200
- Organization: France Telecom Recherche & Developpement
Hi all,
Ok, we suppose it comes from the new native "let in"
construct. Unfortunately, 6.x style could be far more readable,
sometimes.
Require PolyList.
Inductive foo : Set := bar : (list foo)->foo.
(* 6.3 : ok; 7.0 : error *)
Fixpoint interp [x:foo] : nat :=
let f = [l](fold_right plus O (map interp l)) in
Cases x of
| (bar l) => (f l)
end.
(* 6.3 : ok, 7.0 : ok *)
Fixpoint interp [x:foo] : nat :=
Cases x of
| (bar l) => (fold_right plus O (map interp l))
end.
Ciao
--
Cuihtlauac ALVARADO - France Telecom R & D - DTL/MSV/MFL
2, avenue Pierre Marzin - 22307 Lannion Cedex - France
Tel: +33 2 96 05 32 73 - Mob: +33 6 08 10 80 41 - Fax: +33 2 96 05 39 45
- let: 7 vs 6, Cuihtlauac ALVARADO
- Re: let: 7 vs 6, Eduardo Gimenez
Archive powered by MhonArc 2.6.16.