alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Propagate record equations in Adt_rel

Open Halbaroth opened this issue 10 months ago • 0 comments

In #1095, we move record context for constructor term from Records.make to Adt.make. In #1095, the context of X.make is not always propagate to CC(X) in Adt_rel.

Halbaroth avatar Feb 14 '25 16:02 Halbaroth