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 43dbc5c commit 1226ab9Copy full SHA for 1226ab9
hb.elpi
@@ -585,7 +585,7 @@ mk-phant-implicit N Ty PF (phant-term [implicit-arg|AL] (fun N Ty F)) :- !,
585
pred mk-phant-struct i:term, i:term, i:(term -> phant-term), o:phant-term.
586
mk-phant-struct T SI PF (phant-term [implicit-arg, unify-arg|AL] UF) :-
587
get-structure-sort-projection SI Sort,
588
- pi s\ PF s = phant-term AL (F s),
+ (pi s\ PF s = phant-term AL (F s)),
589
UF = {{fun (s : lp:SI) (u : lib:hb.unify lp:T (lp:Sort s)
590
(lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SI)))
591
=> lp:(F s)}}.
0 commit comments