search

AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
24 stars 2 forks source link

Overloading term constructors #14

Closed olynch closed 1 year ago

olynch commented 1 year ago

When I define the theory of monoidal categories, I want to be able to use \otimes for both object composition and morphism composition. I should be able to use type inference to figure out which one I mean when parsing a term, which should be possible by only looking at the type constructors, and then these should get parsed into different de Bruijn levels.

kris-brown commented 1 year ago

Addressed by signatures in https://github.com/AlgebraicJulia/Gatlab.jl/pull/81