Use type classes for operators
Add product constructions for DFA
Add closure properties of regular languages
Prove finite sets are sets
Move definitions that should be ported upstream to a separate directory
Implement multi-tape Turing machines
Make Turing Machines halt only when reaching a final state
Reimplement Turing Machines' tape as an infinite sequence of symbols
Reimplement TM tapes without a head
Add definition of Turing Machines
Add some lemmas to Fin.agda and cleanup
Add TODO keyword for incomplete proofs
Redefine IsFinite and use it as typeclass
Define pushdown finite automata
Rename L to lang in automata and Regex
Add regular expresssion definitions
Also, the sets of languages accepted by regex and by DFAs have been
defined, as well as postulating that they are equal.