feat(Computability): language-preserving maps between NFA and RE#15654
feat(Computability): language-preserving maps between NFA and RE#15654
Conversation
github-actions
bot
added
the
new-contributor
PR summary 3b6ce828b6
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Computability.RegularExpressions | 496 | 626 | +130 (+26.21%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Computability.RegularExpressions |
130 |
Mathlib.Data.FinEnum.Option |
427 |
Mathlib.Computability.GNFA |
627 |
Declarations diff
+ GNFA
+ accepts
+ char
+ charDecidableAccept
+ charDecidableStart
+ charDecidableStep
+ char_correct
+ decidableAccept
+ decidableAux
+ decidableStart
+ decidableStep
+ evalFrom_append
+ evalFrom_subset
+ exists_regularexpression
+ haddDecidableAccept
+ haddDecidableStart
+ haddDecidableStep
+ hadd_correct
+ hmulDecidableAccept
+ hmulDecidableStart
+ hmulDecidableStep
+ hmul_correct
+ hmul_eval₁
+ hmul_eval₂
+ instFinEnumOption
+ instance : HAdd (NFA α σ) (NFA α σ') (NFA α (σ ⊕ σ'))
+ instance : HMul (NFA α σ) (NFA α σ') (NFA α (σ ⊕ σ'))
+ instance : Inhabited (GNFA α σ)
+ instance : One (NFA α σ)
+ instance : Zero (NFA α σ)
+ instance {r : RegularExpression α} : Inhabited r.State
+ kstar
+ kstarDecidableAccept
+ kstarDecidableStart
+ kstarDecidableStep
+ kstar_correct
+ kstar_eval
+ kstar_eval_aux
+ mapEquiv
+ mapEquiv_spec
+ mapEquiv_spec_mpr
+ mapEquiv_trace_aux
+ mapEquiv_trace_equiv_eq_trace
+ matches'_sum
+ mem_sum
+ oneDecidableAccept
+ oneDecidableStart
+ oneDecidableStep
+ one_correct
+ rec'
+ rec'_char
+ rec'_comp
+ rec'_epsilon
+ rec'_plus
+ rec'_star
+ rec'_zero
+ recEmptyOption
+ recOnEmptyOption
+ rip
+ rip_spec
+ rip_trace_aux
+ rip_trace_eq_trace_some
+ toGNFA
+ toNFAStateCard
+ toNFAStateCard_pos
+ toNFAStateFinEnum
+ toNFAX
+ toNFA_spec
+ toRegularExpression
+ toRegularExpressionX
+ toRegularExpression_spec
+ trace
+ zeroDecidableAccept
+ zeroDecidableStart
+ zeroDecidableStep
+ zero_correct
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
This PR/issue depends on: |
ghost
added
the
blocked-by-other-PR
joneugster
added
the
t-computability
leanprover-community-bot-assistant
added
the
merge-conflict
meithecatte
added
the
awaiting-zulip
|
Relevant Zulip discussion: #mathlib4 > Regular languages: the review queue |
4 participants
Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs
Last chunk of #12648