I’m currently working through the Lists portion of Logical Foundations and as I’m working through the “Lists Of Numbers” portion I came to the exercise to build an alternate function. This one:
Fixpoint alternate (l1 l2 : natlist) : natlist
(* REPLACE THIS LINE WITH “:= your_definition .” *). Admitted.
This is what I’ve gotten so far:
Fixpoint alternate (l1 l2 :natlist) : natlist match l1,l2 with | nil, nil => nil | _, nil => l1 | nil,_ => l2 | h::t, h'::t' => [h] ++ [h'] ++ (alternate t t') end.
So two questions:
1.) Is the syntax
2.) The author mentions in the text:
Coq’s requirement that all Fixpoint definitions be “obviously terminating.”
When I attempt to run the code, I get:
The reference alternate was not found in the current environment.
Is this what the author is talking about or is it a different error?