[TC] add comment

LPCIC · Sep 30, 2024 · ede3b19 · ede3b19
1 parent 05c9567
commit ede3b19
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
@@ -111,6 +111,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
+    % [goal T T' L] takes a term T and returns a new term T' where problematic
+    % subterms (see this: https://dl.acm.org/doi/10.1145/3678232.3678233)
+    % are replaced with fresh variables. The list of links is L
     pred goal i:term, o:term, o:list prop.
     :name "compile-goal"
     goal Goal Goal' Links :-