pat: some doc

aya-prover · Jan 4, 2025 · 66bd092 · 66bd092
1 parent d806db6
commit 66bd092
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -317,6 +317,12 @@ public enum Kind {
       patterns.next();    // consume pattern
     }
 
+    // now: ! patterns.hasNext()
+    // or patterns.hasNext() && ! telescope.hasNext() && patterns.isFromPusheen()
+    // or patterns.hasNext() && telescope.hasNext() && patterns.isFromPusheen() && telescope.isFromPusheen()
+
+    // all not pusheen patterns have their parameters
+
     // is there any explicit parameters?
     var generated = findNextParam(null, p ->
         p.explicit()