Commit dd4c99da authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

amelioration seance4

parent 5ac8bfba
......@@ -91,7 +91,7 @@ Check ((1,2),(3,4)) : bintree nat 2.
Fixpoint sumtree n : bintree nat n -> nat :=
match n with
| 0 => fun a => a
| S n => fun a => let (g,d) := a in sumtree n g + sumtree n d
| S n => fun '(g,d) => sumtree n g + sumtree n d
end.
(** Et pour mettre les données aux noeuds au lieu des feuilles : *)
......@@ -102,9 +102,15 @@ Inductive unit : Type := Tt. (* Un type singleton pour les feuilles *)
Fixpoint bintree' (A:Type) n :=
match n with
| 0 => unit
| S n => (bintree A n * A * bintree A n)%type
| S n => (bintree' A n * A * bintree' A n)%type
end.
Fixpoint sumtree' n : bintree' nat n -> nat :=
match n with
| 0 => fun Tt => 0
| S n => fun '(g,a,d) => sumtree' n g + a + sumtree' n d
end.
(** NB: on a utilisé ici des triplets Coq, qui ne sont pas
primitifs (paires de paires). On aurait plus aussi définir
un type inductif ad-hoc. *)
......@@ -213,6 +219,7 @@ Check (Vcons 0 (Vcons 2 (Vcons 3 Vnil))).
(** Mais cet argument [n] est toujours là en interne: *)
Set Printing All.
Check (Vcons 0 (Vcons 2 (Vcons 3 Vnil))).
Check (cons 0 (cons 2 (cons 3 nil))).
Unset Printing All.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment