Экземпляр класса типов Ord для опции

Question

В томе 4 Основ программного обеспечения "QuickChick" у нас есть следующее упражнение:

Class Ord A `{Eq A} : Type :=
{
    le : A -> A -> bool
}.

(* Define [Ord] instances for options and pairs. *)
(* So I am trying to do it *)

Instance optionOrd {A : Type} `{Ord A} `{Eq (option A)} : Ord (option A) :=
{
  le := fun (opt1 opt2 : option A) =>
          match opt1 with
          | None => match opt2 with
                   | None => true
                   | Some a => true
                   end
          | Some a1 => match opt2 with
                      | None => false
                      | Some a2 => le a1 a2
                      end
          end.
}.

Но выдается ошибка:

Error: Syntax error: '}' expected after [constr:record_declaration]
 (in [vernac:gallina_ext]).

И в нем выделяется match opt1 with.

• Может быть, мое решение довольно примитивное: просто шаблон соответствует всем возможным случаям. Есть что-нибудь лучше?

• Что вызывает эту синтаксическую ошибку?

Answer 1

Просто удалите . после последнего end.