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

chore: fix tests

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-16 13:33:35 +02:00
parent 6982536108
commit 6f096e0f0d
2 changed files with 5 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/Reformat/Input.lean
View file

@ -186,13 +186,9 @@ class Inhabited (α : Sort u) :=
opaque arbitrary (α : Sort u) [s : Inhabited α] : α :=
@Inhabited.default α s
instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {
default := fun _ => arbitrary β
}
instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {default := fun _ => arbitrary β}
instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {
default := fun a => arbitrary (β a)
}
instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) := {default := fun a => arbitrary (β a)}
/-- Universe lifting operation from Sort to Type -/
structure PLift (α : Sort u) : Type u :=
@ -210,9 +206,7 @@ structure PointedType :=
(type : Type u)
(val : type)
instance : Inhabited PointedType.{u} := {
default := { type := PUnit.{u+1}, val := ⟨⟩ }
}
instance : Inhabited PointedType.{u} := {default := { type := PUnit.{u+1}, val := ⟨⟩ }}
/-- Universe lifting operation -/
structure ULift.{r, s} (α : Type s) : Type (max s r) :=

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

@ -32,8 +32,8 @@ StxQuot.lean:18:15: error: expected term
"`a._@.UnhygienicMain._hyg.1"
"(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(num \"0\")] \"}\")"
"#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]"
"(Term.structInst\n \"{\"\n []\n [(group\n (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n [])]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [(group\n (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n [])]\n (Term.optEllipsis [])\n []\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)]\n (Term.optEllipsis [])\n []\n \"}\")"
"(Command.section \"section\" [])"
"(Command.section \"section\" [`foo._@.UnhygienicMain._hyg.1])"
"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))"