minor: remove comment + move count-prod in base.elpi

LPCIC · May 13, 2024 · d1f6f60 · d1f6f60
1 parent b055d23
commit d1f6f60
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 13 deletions.
diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
@@ -127,6 +127,10 @@ pred length-nat i:list A, o:nat.
 length-nat [] z.
 length-nat [_|L] (s N) :- length-nat L N.
 
+pred count-prod i:term , o:nat.
+count-prod (prod _ _ B) (s N) :- !, pi x\ count-prod (B x) N.
+count-prod _ z.
+
 pred close-prop i:(A -> list prop), o:list prop.
 close-prop (x\ []) [] :- !.
 close-prop (x\ [X | Xs x]) [X| Xs'] :- !, close-prop Xs Xs'.

diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
@@ -63,16 +63,6 @@ namespace tc {
       coq.say "Charging" (copy Y X),
       (copy Y X :- !) => relocate Xs Ys T T'.
 
-    % constraint eta uvar relocate fun {
-    %   rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1)) 
-    %       \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2)) 
-    %       | (
-    %         pi x\ relocate L1 L2 (B2 x) (B2' x),
-    %         coq.say "Will unify" B1 "and" B2'
-    %       )  
-    %   <=> (N1 : G1 ?- B1 = B2').
-    % }
-
     pred collect-store o:list prop.
     pred collect-store-aux i:list prop, o:list prop.
 

diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
@@ -1,9 +1,6 @@
 namespace tc {
 
   namespace precomp {
-    pred count-prod i:term , o:nat.
-    count-prod (prod _ _ B) (s N) :- !, pi x\ count-prod (B x) N.
-    count-prod _ z.
 
     namespace instance {
       % Tells if the current name is a bound variables