AlgebraicJulia / AlgebraicJulia/GATlab.jl
Make renaming not generate as many new scopetags
- 主要語言
- Julia
- 星號
- 43
- 分支
- 4
- PR 合併指標
- 30 天內沒有已合併 PR
描述
There are new features for renaming in the pipeline (https://github.com/AlgebraicJulia/GATlab.jl/pull/147 and https://github.com/AlgebraicJulia/GATlab.jl/pull/146) which suffer from a common problem of generating completely fresh ScopeTags for the renamed theory. Consider the following scenario:

We rename `*` to `+` in both `ThGrp` and `ThAbGrp` (which extends `ThGrp` with a commutativity axiom). With the present setup, it will **not** be the case that `ThAddGrp` will be a proper inclusion of `ThAddAbGrp`.
One way to address this is to make the data to rename `ThGrp` (resp. `ThAbGrp`) be the renaming morphism (as generated by the existing tooling) from `ThMon` to `ThAddMon` as well as an inclusion from `ThMon` into `ThGrp` (resp `ThAbGrp`). This fancier renaming function will make sure to use the fresh scopetags from `ThAddMon` in both `ThAddGrp` and `ThAddAbGrp`.

貢獻指南
這個儲存庫沒有索引到貢獻指南
評估
這個 Issue 還沒有評估資料。