Closed kris-brown closed 9 months ago
Attention: 36 lines
in your changes are missing coverage. Please review.
Comparison is base (
a0c5e58
) 88.25% compared to head (785ae67
) 94.26%.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
TermInCtx and TypeInCtx are made more flexible to take a general context, rather than just a scope. This required making Context take {T, Sig} type parameters.
Previously we had conflicting meanings of
idents
- one was for broadcasting arguments toident
and the other was listing all the idents in a Context. The latter is now calledgetidents
.Also theory maps before required some redundancy in the expressions they parsed, this has been improved so that we can write
compose(f,g) ⊣ [(a,b,c)::Ob,f::Hom(a,b), g::Hom(b,c)] => compose(g, f)
with no explicit RHS context.