In volume 4 of Software foundations "QuickChick" we have the following excercise:
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.
}.
But get an error:
Error: Syntax error: '}' expected after [constr:record_declaration]
(in [vernac:gallina_ext]).
And it highlights match opt1 with
.
Maybe, my solution is quite primitive: it just pattern matches all possible cases. Is there anything better?
What causes this syntax error?
Just remove the .
after the last end
.