Commit fa71fe21 authored by Ralf Jung's avatar Ralf Jung

fix map_list recursive name

parent 833b7228
...@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l", ...@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l",
(** A function that maps a function over all elements of a list: *) (** A function that maps a function over all elements of a list: *)
Definition map_list : val := Definition map_list : val :=
rec: "inc_list" "f" "l" := rec: "map_list" "f" "l" :=
match: "l" with match: "l" with
NONE => #() NONE => #()
| SOME "p" => | SOME "p" =>
let: "x" := Fst !"p" in let: "x" := Fst !"p" in
let: "l" := Snd !"p" in let: "l" := Snd !"p" in
"p" <- ("f" "x", "l");; "p" <- ("f" "x", "l");;
"inc_list" "f" "l" "map_list" "f" "l"
end. end.
Section proof. Section proof.
......
...@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l", ...@@ -38,14 +38,14 @@ Definition sum_inc_list : val := λ: "n" "l",
(** A function that maps a function over all elements of a list: *) (** A function that maps a function over all elements of a list: *)
Definition map_list : val := Definition map_list : val :=
rec: "inc_list" "f" "l" := rec: "map_list" "f" "l" :=
match: "l" with match: "l" with
NONE => #() NONE => #()
| SOME "p" => | SOME "p" =>
let: "x" := Fst !"p" in let: "x" := Fst !"p" in
let: "l" := Snd !"p" in let: "l" := Snd !"p" in
"p" <- ("f" "x", "l");; "p" <- ("f" "x", "l");;
"inc_list" "f" "l" "map_list" "f" "l"
end. end.
Section proof. Section proof.
......
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