Commit 2023-04-03 15:27 f85368f4

View on Github →

feat Port/Computability.RegularExpressions (#2306) port of computability.regular_expressions The previous file defined attribute [match_pattern] Mul.mul but this is not allowed in Lean 4

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/RegularExpressions.lean

added theorem RegularExpression.add_rmatch_iff

added theorem RegularExpression.char_rmatch_iff

added theorem RegularExpression.comp_def

added def RegularExpression.deriv

added theorem RegularExpression.deriv_add

added theorem RegularExpression.deriv_char_of_ne

added theorem RegularExpression.deriv_char_self

added theorem RegularExpression.deriv_one

added theorem RegularExpression.deriv_star

added theorem RegularExpression.deriv_zero

added def RegularExpression.map

added theorem RegularExpression.map_id

added theorem RegularExpression.map_map

added def RegularExpression.matchEpsilon

added def RegularExpression.matches'

added theorem RegularExpression.matches'_add

added theorem RegularExpression.matches'_char

added theorem RegularExpression.matches'_epsilon

added theorem RegularExpression.matches'_map

added theorem RegularExpression.matches'_mul

added theorem RegularExpression.matches'_pow

added theorem RegularExpression.matches'_star

added theorem RegularExpression.matches'_zero

added theorem RegularExpression.mul_rmatch_iff

added theorem RegularExpression.one_def

added theorem RegularExpression.one_rmatch_iff

added theorem RegularExpression.plus_def

added def RegularExpression.rmatch

added theorem RegularExpression.rmatch_iff_matches'

added theorem RegularExpression.star_rmatch_iff

added theorem RegularExpression.zero_def

added theorem RegularExpression.zero_rmatch

added inductive RegularExpression