Commit 2024-07-14 20:04 73756969

View on Github →

feat: DFA.acceptsFrom, DFA.map, DFA.equiv (#11372) acceptsFrom is used in #11311 to define left quotients.

Estimated changes

modified def DFA.accepts
added def DFA.acceptsFrom
added theorem DFA.accepts_comap
added theorem DFA.accepts_reindex
added def DFA.comap
added theorem DFA.comap_id
added theorem DFA.comap_reindex
modified def DFA.evalFrom
added theorem DFA.evalFrom_comap
added theorem DFA.evalFrom_reindex
added theorem DFA.eval_comap
added theorem DFA.eval_reindex
modified theorem DFA.mem_accepts
added theorem DFA.mem_acceptsFrom
added def DFA.reindex
added theorem DFA.reindex_refl
added theorem DFA.symm_reindex