AlgebraicJulia / AlgebraicJulia/GATlab.jl

Make renaming not generate as many new scopetags

未關閉
#148 0 則留言 0 個 reaction 已指派 0 人 在 GitHub 檢視
enhancement
主要語言
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:

![Screenshot 2024-03-20 at 10 49 45 AM](https://github.com/AlgebraicJulia/GATlab.jl/assets/27834499/b8550463-e060-48de-824e-6a3df864b722)

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`.

![Screenshot 2024-03-20 at 10 50 59 AM](https://github.com/AlgebraicJulia/GATlab.jl/assets/27834499/7a18abb3-db5a-4fdf-adb2-2d58c0e2772b)

貢獻指南

這個儲存庫沒有索引到貢獻指南

評估

這個 Issue 還沒有評估資料。

把新 issue 寄到你的電子郵件信箱

精選適合新手參與的 GitHub issue 摘要。