From 6fb0ae91c7856fbe569c8a78057d67700b3f1be3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 27 Oct 2020 16:47:09 +0100
Subject: [PATCH] test: fix tests

---
 .../termparsertest1.lean.expected.out         | 22 ++++++++++++-------
 tests/lean/Reformat.lean.expected.out         | 21 ++++++++----------
 tests/lean/StxQuot.lean.expected.out          |  4 ++--
 3 files changed, 25 insertions(+), 22 deletions(-)

diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index b98074d984..8dbea4881d 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -41,21 +41,27 @@ suffices h : p x y from f x; g this
 show p x y from f x
 (Term.show "show" (Term.app `p [`x `y]) (Term.fromTerm "from" (Term.app `f [`x])))
 fun x y => f y x
-(Term.fun "fun" [`x `y] "=>" (Term.app `f [`y `x]))
+(Term.fun "fun" (Term.basicFun [`x `y] "=>" (Term.app `f [`y `x])))
 fun (x y : Nat) => f y x
-(Term.fun "fun" [(Term.paren "(" [(Term.app `x [`y]) [(Term.typeAscription ":" `Nat)]] ")")] "=>" (Term.app `f [`y `x]))
+(Term.fun
+ "fun"
+ (Term.basicFun
+  [(Term.paren "(" [(Term.app `x [`y]) [(Term.typeAscription ":" `Nat)]] ")")]
+  "=>"
+  (Term.app `f [`y `x])))
 fun (x, y) => f y x
-(Term.fun "fun" [(Term.paren "(" [`x [(Term.tupleTail "," [`y])]] ")")] "=>" (Term.app `f [`y `x]))
+(Term.fun "fun" (Term.basicFun [(Term.paren "(" [`x [(Term.tupleTail "," [`y])]] ")")] "=>" (Term.app `f [`y `x])))
 fun z (x, y) => f y x
-(Term.fun "fun" [`z (Term.paren "(" [`x [(Term.tupleTail "," [`y])]] ")")] "=>" (Term.app `f [`y `x]))
+(Term.fun "fun" (Term.basicFun [`z (Term.paren "(" [`x [(Term.tupleTail "," [`y])]] ")")] "=>" (Term.app `f [`y `x])))
 fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z
 (Term.fun
  "fun"
- [(Term.anonymousCtor "⟨" [`x "," `y] "⟩") (Term.anonymousCtor "⟨" [`z "," `w] "⟩")]
- "=>"
- (Term.app `f [`y `x `w `z]))
+ (Term.basicFun
+  [(Term.anonymousCtor "⟨" [`x "," `y] "⟩") (Term.anonymousCtor "⟨" [`z "," `w] "⟩")]
+  "=>"
+  (Term.app `f [`y `x `w `z])))
 fun (Prod.mk x y) => f y x
-(Term.fun "fun" [(Term.paren "(" [(Term.app `Prod.mk [`x `y]) []] ")")] "=>" (Term.app `f [`y `x]))
+(Term.fun "fun" (Term.basicFun [(Term.paren "(" [(Term.app `Prod.mk [`x `y]) []] ")")] "=>" (Term.app `f [`y `x])))
 { x := 10, y := 20 }
 (Term.structInst
  "{"
diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out
index 2c53eda242..be610d609b 100644
--- a/tests/lean/Reformat.lean.expected.out
+++ b/tests/lean/Reformat.lean.expected.out
@@ -1088,18 +1088,15 @@ instance  (p : Prop) : Subsingleton p :=
 
 instance  (p : Prop) : Subsingleton (Decidable p) :=
 Subsingleton.intro
-  fun d₁ =>
-    match d₁ with 
-    | (isTrue t₁) =>
-      fun d₂ =>
-        match d₂ with 
-        | (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl
-        | (isFalse f₂) => absurd t₁ f₂
-    | (isFalse f₁) =>
-      fun d₂ =>
-        match d₂ with 
-        | (isTrue t₂) => absurd t₂ f₁
-        | (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl 
+  fun
+  | (isTrue t₁) =>
+    fun
+    | (isTrue t₂) => proofIrrel t₁ t₂ ▸ rfl
+    | (isFalse f₂) => absurd t₁ f₂
+  | (isFalse f₁) =>
+    fun
+    | (isTrue t₂) => absurd t₂ f₁
+    | (isFalse f₂) => proofIrrel f₁ f₂ ▸ rfl 
 
 theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
   [h₃ : ∀  (h : p), Subsingleton (h₁ h)] [h₄ : ∀  (h : ¬p), Subsingleton (h₂ h)] :
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 0fafddbbf5..d5c5fdc7ca 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -5,7 +5,7 @@
 "(Term.add <missing> \"+\" (numLit \"1\"))"
 "(Term.add <missing> \"+\" (numLit \"1\"))"
 "(Term.add (numLit \"1\") \"+\" (numLit \"1\"))"
-"(Term.fun \"fun\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1)"
+"(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\"))))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\"))))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\"))))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
@@ -18,7 +18,7 @@
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\"))))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\"))))]"
 "0"
 "1"
-"(Term.fun\n \"fun\"\n [`a._@.UnhygienicMain._hyg.1\n  (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\")]\n \"=>\"\n (numLit \"1\"))"
+"(Term.fun\n \"fun\"\n (Term.basicFun\n  [`a._@.UnhygienicMain._hyg.1\n   (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\")]\n  \"=>\"\n  (numLit \"1\")))"
 "#[(Term.paren \"(\" [`a._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\"), `b._@.UnhygienicMain._hyg.1]"
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.forall \"∀\" [(Term.simpleBinder [(Term.hole \"_\")])] \",\" `c._@.UnhygienicMain._hyg.1)"