few comments

LPCIC · Oct 17, 2018 · 1912082 · 1912082
1 parent 92425f0
commit 1912082
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/derive/induction.elpi b/derive/induction.elpi
@@ -12,6 +12,7 @@ subst A B :- copy A B, !.
 % local db associating to each constructor the hypothesis to be used
 type induction-hyp-db term -> term -> prop.
 
+% TODO: fix for W (strip under lambda + map-db under forall)
 strip-last-arg (app [Hd|Args]) X R :-
   appendR Prefix [X] Args,
   if (Prefix = []) (R = Hd) (mk-app Hd Prefix R).

diff --git a/theories/derive/tests/test_induction.v b/theories/derive/tests/test_induction.v
@@ -12,7 +12,9 @@ Elpi derive.induction Coverage.option.
 Elpi derive.induction Coverage.pair.
 Elpi derive.induction Coverage.seq.
 Elpi derive.induction Coverage.tree.
+(* TODO: non uniform params *)
 Fail Elpi derive.induction Coverage.nest.
+(* TODO: w *)
 Fail Elpi derive.induction Coverage.w.
 Elpi derive.induction Coverage.vect.
 Fail Elpi derive.induction Coverage.dyn.