Skip to Content.
Sympa Menu

coq-club - let: 7 vs 6

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

let: 7 vs 6


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page