search

jamievicary / globular

Globular
37 stars 9 forks source link

Feature: allow merging of two cells with the same type #18

Open jamievicary opened 8 years ago

jamievicary commented 8 years ago

Given two generators A and B in a project with exactly the same type (that is, s(A)=s(B) and t(A)=t(B)), this option would merge them, so that all references to B in other cells and diagrams are replaced with references to A, and the cell B is deleted.

jamievicary commented 8 years ago

This would involve the development of a unification procedure for types.