refactor: Language as a one-field structure#36934
refactor: Language as a one-field structure#36934Parcly-Taxel wants to merge 15 commits intoleanprover-community:masterfrom
Language as a one-field structure#36934Conversation
PR summary 7555c791b1Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 6795 | -9 | backward.isDefEq.respectTransparency |
Current commit 3ee298d586
Reference commit 7555c791b1
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
An alternative I tried and failed to do in the past would be to make SetSemiring a structure and Language an abbrev for it. |
|
This pull request has conflicts, please merge |
This will only work if |
| @[simp] lemma language_reverse : g.reverse.language = g.language.reverse := by | ||
| ext | ||
| simp [language, Language.reverse_eq_image, List.reverse_eq_iff] |
There was a problem hiding this comment.
If you've set things up correctly, then this proof shouldn't need changing
There was a problem hiding this comment.
I don't know how to do this.
Co-authored-by: Yaël Dillies <[email protected]>
I meant |
|
I tend to agree then. @Parcly-Taxel, could you investigate this solution? |
|
|
This pull request has conflicts, please merge |
|
This PR/issue depends on:
|
I came across definitional equality problems when trying to prove the following as part of a challenge from my PhD advisor:
This refactor resolves said defeq problems by making
Languageinto a one-field structure withtoSetandofSet.SetSemiring#37603