The Coq mailing list

[roconnor AT theorem.ca]

Would anything bad happen if iota or beta reduction was extending to directly 
fill in parametric parameters of CoFixpoints?

The use case that vas and I have been considering is below.
The idea would be to be able to define append without having to define 
append0.

CoInductive LList (A:Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.

Section Foo.

Variable A:Set.
Variable l2:LList A.

CoFixpoint append0 l1 : LList A :=
  match l1 with
  | LNil => l2
  | LCons x xs => LCons A x (append0 xs)
  end.

End Foo.

Definition append (A:Set) (l1 l2:LList A) := append0 A l2 l1.

CoFixpoint cycle (A:Set) (input : LList A) : LList A :=
  match input with
  | LNil => LNil A
  | LCons x xs => LCons A x (append A xs (cycle A input))
  end.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''