Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 11:04 1db70a89

View on Github →

feat(computability/regular_expressions): define regular expressions (#5036) Very basic definitions for regular expressions

Estimated changes

Created src/computability/regular_expressions.lean

added theorem regular_expression.add_rmatch_iff

added theorem regular_expression.char_rmatch_iff

added theorem regular_expression.comp_def

added def regular_expression.deriv

added def regular_expression.match_epsilon

added def regular_expression.matches

added theorem regular_expression.matches_add_def

added theorem regular_expression.matches_epsilon_def

added theorem regular_expression.matches_mul_def

added theorem regular_expression.matches_star_def

added theorem regular_expression.matches_zero_def

added theorem regular_expression.mul_rmatch_iff

added theorem regular_expression.one_def

added theorem regular_expression.one_rmatch_iff

added theorem regular_expression.plus_def

added def regular_expression.rmatch

added theorem regular_expression.rmatch_iff_matches

added theorem regular_expression.star_rmatch_iff

added theorem regular_expression.zero_def

added theorem regular_expression.zero_rmatch

added inductive regular_expression