Forgot to set this field in the example, thank you for spotting this! EDIT: fixed

I'm attempting to load the sample code in Coq v8.12.2 and I'm getting an error.

Inductive A := a | b.
Inductive State := Q0 | Q1 | Q2 | QA.

Definition example_NFA : NFA A State :=
{|
delta := fun arr => match arr with
| eps Q0 Q1
| sym Q1 a Q2
| sym Q2 b Q1
| sym Q0 a QA => True
| _ => False
end ;
q0 := Q0 ;
F := fun q => q = Q1 / q = QA
|}.

(** Error below *)

The following term contains unresolved implicit arguments:
{|
state_fin := ?state_fin;
delta := fun arr : arrow A State =>
match arr with
| sym Q0 a QA | sym Q1 a Q2 | sym Q2 b Q1 | eps Q0 Q1 => True
| _ => False
end;
q0 := Q0;
F := fun q : State => q = Q1 / q = QA |}
More precisely:

• ?state_fin: Cannot infer field state_fin of record NFA.

Quite concise compared to my solution, nice!

An excellent kata! I enjoyed it a lot.