chore: fix tests

This commit is contained in:
Leonardo de Moura 2021-04-05 12:35:52 -07:00
parent fb38955be2
commit fbd6adaf21
3 changed files with 7 additions and 5 deletions

View file

@ -229,7 +229,7 @@
Prod.snd : {α β : Type} → α × β → β @ ⟨28, 4⟩-⟨28, 5⟩
Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨28, 5⟩-⟨28, 6⟩
1 : Nat @ ⟨28, 6⟩-⟨28, 7⟩
[.] Array.getOp s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 8⟩
[.] Array.getOp s.snd 1 : Array Nat @ ⟨28, 2⟩-⟨28, 8⟩ : some Array.{0} Nat
Array.push : {α : Type} → Array αα → Array α @ ⟨28, 9⟩-⟨28, 13⟩
s.fst : Nat @ ⟨28, 14⟩-⟨28, 17⟩
s : Nat × Array (Array Nat) @ ⟨28, 14⟩-⟨28, 15⟩
@ -242,11 +242,11 @@
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
[.] arg : B @ ⟨31, 2⟩-⟨31, 18⟩
[.] arg : B @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
B.pair : B → A × A @ ⟨31, 6⟩-⟨31, 10⟩
[.] arg.pair : A × A @ ⟨31, 2⟩-⟨31, 18⟩
[.] arg.pair : A × A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
Prod.fst : {α β : Type} → α × β → α @ ⟨31, 11⟩-⟨31, 14⟩
[.] arg.pair.fst : A @ ⟨31, 2⟩-⟨31, 18⟩
[.] arg.pair.fst : A @ ⟨31, 2⟩-⟨31, 18⟩ : some Nat
A.val : A → Nat → Nat @ ⟨31, 15⟩-⟨31, 18⟩
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩

View file

@ -23,7 +23,7 @@
{"label": "ax1", "detail": "?a ≤ ?b → ?a - ?a ≤ ?b - ?b"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completion2.lean"},
"position": {"line": 35, "character": 22}}
"position": {"line": 37, "character": 22}}
{"items":
[{"label": "ex2", "detail": "?a ≤ ?b → ?a + 2 ≤ ?b + 2"},
{"label": "ex3", "detail": "?a ≤ ?b → ?c ≤ ?d → ?a + ?c ≤ ?b + ?d"},

View file

@ -11,3 +11,5 @@ inductive Nat : Type
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat
tokenErrors.lean:17:1: error: unterminated comment
tokenErrors.lean:17:0-17:1: error: unexpected command