We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 33ebd03 commit b6a2eaaCopy full SHA for b6a2eaa
apps/tc/elpi/ho_compile.elpi
@@ -121,6 +121,7 @@ namespace tc {
121
pred clean-term i:term, o:term.
122
clean-term A B :-
123
(pi t s r \ copy (tc.maybe-eta-tm t s) r :- !, copy t r, !) =>
124
+ (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
125
(pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
126
(pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
127
std.assert! (copy A B) "[TC] clean-term error".
0 commit comments