A modified form of a part of reglang. https://github.com/coq-community/reglang/ Made as an attempt to get familiar with mathcomp. Atoms are boolean functions instead of symbols. NFA construction proven correct. Build with: $ nix-shell $ dune build