max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: fix tests

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-27 16:47:09 +01:00
parent bb8977b0f8
commit 6fb0ae91c7
3 changed files with 25 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
tests/compiler/termparsertest1.lean.expected.out
View file

@ -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
"{"

21
tests/lean/Reformat.lean.expected.out
View file

@ -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)] :

4
tests/lean/StxQuot.lean.expected.out
View file

@ -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)"