Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 18:49 dee49588

View on Github →

feat(computability/*): Automata lemmas (#13194) A bunch of missing API for language, regular_expression, DFA, NFA, ε_NFA.

Estimated changes

modified def DFA.eval
added theorem DFA.eval_from_nil
added theorem DFA.eval_nil
added theorem DFA.eval_singleton
modified def NFA.eval
added theorem NFA.eval_from_nil
added theorem NFA.eval_nil
added theorem NFA.eval_singleton
modified theorem NFA.mem_step_set
modified def NFA.step_set
added theorem NFA.step_set_empty
added theorem ε_NFA.accept_one
added theorem ε_NFA.accept_zero
modified def ε_NFA.accepts
added theorem ε_NFA.eval_from_empty
added theorem ε_NFA.eval_from_nil
added theorem ε_NFA.eval_nil
added theorem ε_NFA.eval_singleton
added theorem ε_NFA.start_one
added theorem ε_NFA.start_zero
added theorem ε_NFA.step_one
modified def ε_NFA.step_set
added theorem ε_NFA.step_set_empty
added theorem ε_NFA.step_zero
modified inductive ε_NFA.ε_closure
added theorem ε_NFA.ε_closure_univ
added theorem language.join_mem_star
modified theorem language.mem_add
modified theorem language.mem_mul
modified theorem language.mem_one
modified theorem language.mem_star
modified theorem language.nil_mem_one
added theorem language.nil_mem_star