pat-lam: fix test

cli-impl/src/test/resources/negative/ExprTyckError.txt

@@ -46,7 +46,7 @@ In file $FILE:2:19 ->
     │                      ╰──────╯
 
 Error: The following abstraction is not good:
-         \ x ⇒ x
+         fn x ⇒ x
        because the type being expected is not a Pi/Path type, but instead:
          Type 0
 
@@ -225,11 +225,11 @@ In file $FILE:3:4 ->
 
 Error: The following application is not good:
          match a {
-          | _ ⇒ \ x ⇒ x
+          | _ ⇒ fn x ⇒ x
         } 1
        because the type of what you applied is not a Pi/Path type, but instead:
          <type of `match a {
-          | _ ⇒ \ x ⇒ x
+          | _ ⇒ fn x ⇒ x
         }`>
 
 2 error(s), 0 warning(s).

cli-impl/src/test/resources/negative/GoalAndMeta.txt

@@ -281,7 +281,7 @@ In file $FILE:11:12 ->
      │               ╰───────────────────────────╯
 
 Error: Cannot check the expression
-         pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _)
+         pmap (fn _ ⇒ x :> _) (++-assoc' _ _ _)
        of type
          (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m
         o _ ys zs)

cli-impl/src/test/resources/shared/src/data/sum/base.aya

@@ -11,7 +11,7 @@ def Sum-rec
   (P : Type)
   (lrec : A -> P)
   (rrec : B -> P)
-  : P => Sum-ind e (fn _e => P) (fn a _p => lrec a) (fn b _p => rrec b)
+  : P => Sum-ind e (fn _ => P) (fn a, _ => lrec a) (fn b, _ => rrec b)
 
 def Sum-ind
   (e : Sum A B)

cli-impl/src/test/resources/shared/src/relation/binary/path.aya

@@ -8,7 +8,7 @@ def refl {a : A} : a = a => \i => a
 def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i)
 def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
 
-def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i, a => p a i
 
 def pmapd {A : I -> Type} (B : ∀ i -> A i -> Type)
     (f : ∀ i -> ∀ (a : A i) -> B i a) {a b : _} (p : Path A a b)

cli-impl/src/test/resources/success/src/PLFA.aya

@@ -12,7 +12,7 @@ def deMorgan-law => Fn (A B : Type) -> (neg (Sig (neg A) ** (neg B))) -> Sum A B
 
 @suppress(MostGeneralSolution)
 def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
-  fn tyA tyB np =>
+  fn tyA, tyB, np =>
     Sum-rec (lem tyA)
     _
     (fn A => A)
@@ -23,7 +23,7 @@ def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
       (fn ¬B => exfalso (np (¬A, ¬B))))
 
 def deMorgan-law=>imply-as-lor (dml : deMorgan-law) : imply-as-lor =>
-  fn tyA tyB f =>
+  fn tyA, tyB, f =>
     dml (neg tyA) tyB (fn p => p.1 (fn A => exfalso (p.2 (f A))))
 
 def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
@@ -32,15 +32,15 @@ def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
 @suppress(MostGeneralSolution)
 def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law =>
   // f : ((A -> B) -> A)
-  fn tyA tyB f => Sum-rec
+  fn tyA, tyB, f => Sum-rec
     (imply-as-lor=>LEM ial tyA)
     _
     (fn A => A)
     (fn nA => f (fn A => exfalso (nA A)))
 
 @suppress(MostGeneralSolution)
 def peirce-law=>double-neg-elim (pl : peirce-law) : double-neg-elim =>
-  fn tyA ¬¬A =>
+  fn tyA, ¬¬A =>
     pl tyA Empty (fn ¬A => exfalso (¬¬A ¬A))
 
 @suppress(MostGeneralSolution)

cli-impl/src/test/resources/success/src/Pattern.aya

@@ -53,5 +53,5 @@ module PullRequest1268 {
   // unpi: D d0 -> d1
   @suppress(LocalShadow)
   def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a, b
-  | a => fn b D => id D
+  | a => fn b, D => id D
 }

syntax/src/main/java/org/aya/prettier/ConcretePrettier.java

@@ -115,7 +115,6 @@ yield visitConcreteCalls(assoc,
 
         yield checkParen(outer, visitLambda(dummyCls), Outer.BinOp);
       }
-      // TODO
       case Expr.IrrefutableLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
       case Expr.Hole expr -> {
         if (!expr.explicit()) yield Doc.symbol(Constants.ANONYMOUS_PREFIX);
@@ -492,13 +491,6 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep(
   private @NotNull Doc visitLambda(@NotNull Pattern.Clause clause) {
     var prelude = MutableList.of(LAMBDA);
     prelude.append(clause(clause));
-    var body = clause.expr.get().data();
-
-    if (!(body instanceof Expr.Hole hole && !hole.explicit())) {
-      prelude.append(FN_DEFINED_AS);
-      prelude.append(term(Outer.Free, body));
-    }
-
     return Doc.sep(prelude);
   }
 }

syntax/src/main/java/org/aya/syntax/concrete/Pattern.java

@@ -30,7 +30,13 @@
 public sealed interface Pattern extends AyaDocile {
   void forEach(@NotNull PosedConsumer<@NotNull Pattern> f);
   interface Salt { }
+
+  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.IrrefutableLam] in desugarer.
+  ///
+  /// @see Pattern.Bind
+  /// @see Pattern.CalmFace
   interface Refutable {
+    /// Returns the [LocalVar] this [Pattern] introduced, with [SourcePos] {@param pos} if it doesn't have one.
     @NotNull LocalVar toLocalVar(@NotNull SourcePos pos);
   }