chore(*): fix tests
This commit is contained in:
parent
27f6f2a951
commit
a591e35544
4 changed files with 5 additions and 4 deletions
1
src/tests/shell/.gitignore
vendored
Normal file
1
src/tests/shell/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
*.produced.out
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
{"message":"file invalidated","response":"ok","seq_num":0}
|
||||
{"record":{"full-id":"f","source":{"column":10,"line":1},"type":"Type"},"response":"ok","seq_num":1}
|
||||
{"record":{"full-id":"f","source":{"column":10,"file":"f","line":1},"type":"Type"},"response":"ok","seq_num":1}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[reducible]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
|
||||
{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
|
||||
{"message":"file invalidated","response":"ok","seq_num":0}
|
||||
{"record":{"source":},"response":"ok","seq_num":2}
|
||||
{"record":{"doc":"reducible"},"response":"ok","seq_num":5}
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
m n : ℕ,
|
||||
i : F m
|
||||
⊢ F.raise (succ n) m i = F.suc (m + n) (F.raise n m i)
|
||||
unification_hints2.lean:7:8: warning: declaration '_example' uses sorry
|
||||
unification_hints2.lean:7:0: warning: declaration '[anonymous]' uses sorry
|
||||
α : Type u,
|
||||
a b : α,
|
||||
l₁ l₂ : list α,
|
||||
i : G α l₂
|
||||
⊢ G.raise α (a :: l₁) l₂ i = G.cons α a (l₁ ++ l₂) (G.raise α l₁ l₂ i)
|
||||
unification_hints2.lean:24:8: warning: declaration '_example' uses sorry
|
||||
unification_hints2.lean:24:0: warning: declaration '[anonymous]' uses sorry
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue