The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 01/10/2012 04:26 PM, Edsko de Vries wrote:
> Instance permute_term : Permute Term := fix ...
>
> but still I cannot use permute in the body (it complains that no
> instance of Permute Term is known). The work around is the same as for
> the inductive definitions, I now have whole slews of lemmas of the form
Does the following help you out?

Definition Permutation T := (T -> T).

Class Permute A T :=
  permute : Permutation A -> T -> T.

Definition permute_list {A} : Permute A  (list A) :=
  fix aux (p : Permutation A) (l : list A) :=
    match l with
      | nil => nil
      | cons a l => cons (p a) (@permute _ _ aux p l)
    end.
Existing Instance permute_list.

Here I give the Permute instance by hand.