Lexicographic ordering on lists (with functors)

Construct a functor associed with the lexicographic ordering on lists.
Require Export DecOrders.

(* Lexicographic ordering for lists *)

Module List_Order (D: DEC_ORDER) <: DEC_ORDER with Definition
  A := list D.A .

You may require this module

Solution

This file