revert: syntax changes in stdlib (sorry)

aya-prover · Jan 20, 2025 · 7c126ec · 7c126ec
1 parent 47ba19a
commit 7c126ec
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/cli-impl/src/test/resources/shared/src/data/sum/base.aya b/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 _ => P) (fn a, _ => lrec a) (fn b, _ => rrec b)
+  : P => Sum-ind e (fn _e => P) (fn a _p => lrec a) (fn b _p => rrec b)
 
 def Sum-ind
   (e : Sum A B)

diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya 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)

diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya 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)

diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/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
 }