...
 
Commits (2)
......@@ -8,7 +8,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
.PHONY: clean
......
......@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l",
(** A function that maps a function over all elements of a list: *)
Definition map_list : val :=
rec: "inc_list" "f" "l" :=
rec: "map_list" "f" "l" :=
match: "l" with
NONE => #()
| SOME "p" =>
let: "x" := Fst !"p" in
let: "l" := Snd !"p" in
"p" <- ("f" "x", "l");;
"inc_list" "f" "l"
"map_list" "f" "l"
end.
Section proof.
......
......@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l",
(** A function that maps a function over all elements of a list: *)
Definition map_list : val :=
rec: "inc_list" "f" "l" :=
rec: "map_list" "f" "l" :=
match: "l" with
NONE => #()
| SOME "p" =>
let: "x" := Fst !"p" in
let: "l" := Snd !"p" in
"p" <- ("f" "x", "l");;
"inc_list" "f" "l"
"map_list" "f" "l"
end.
Section proof.
......