Software Foundations/Logical Foundations Exercise

Using Coq
1

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 h::t,h'::t' correct?

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?

2

You’re missing the “:=”

Gaëtan Gilbert

1 Like
3

Wow. I feel so dumb! Thank you!