Open TOTBWF opened 1 month ago
Could we have a test/reproducer for the printing issues with, say, binary products?
I think @plt-amy had a good real world example in https://gist.github.com/plt-amy/9f1efaaef2fe15baf4965be21e60994b, we could use the code that generated the nightmare for that
I guess things like δ-natural
can serve as test cases. Without this PR the goal is
is-product.⟨ Product.has-is-product (all-products y y) , id ⟩
id
∘ f
≡
is-product.⟨ Product.has-is-product (all-products y y) ,
f ∘ Product.π₁ (all-products x x) ⟩
(f ∘ Product.π₂ (all-products x x))
∘ is-product.⟨ Product.has-is-product (all-products x x) , id ⟩ id
With this PR it becomes ⟨ id , id ⟩ ∘ f ≡ ⟨ f ∘ π₁ , f ∘ π₂ ⟩ ∘ ⟨ id , id ⟩
. Much better!
Description
This PR flattens out
Binary-products
et. al into flat records to get better printing.Currently, this is a draft to get API feedback!
Checklist
Before submitting a merge request, please check the items below:
support/sort-imports.hs
(ornix run --experimental-features nix-command -f . sort-imports
).If your change affects many files without adding substantial content, and you don't want your name to appear on those pages (for example, treewide refactorings or reformattings), start the commit message and PR title with
chore:
.