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:
Leonardo de Moura 2022-09-24 15:17:06 -07:00
parent cd6508ef5f
commit 871644fe8b
3 changed files with 14 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
tests/lean/holes.lean.expected.out
View file

@ -1,15 +1,4 @@
holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected
holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
context:
case hole
x : Nat
y : Nat
⊢ Nat
holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
context:
x : Nat
y : Nat
⊢ Nat
holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
@g Nat (?m x) x
context:
@ -20,6 +9,17 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
context:
x : Nat
⊢ Type
holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
context:
x : Nat
y : Nat
⊢ Nat
holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
context:
case hole
x : Nat
y : Nat
⊢ Nat
holes.lean:13:10-13:11: error: failed to infer binder type
holes.lean:15:16-15:17: error: failed to infer binder type
holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument

2
tests/lean/linterUnusedVariables.lean.expected.out
View file

@ -3,8 +3,8 @@ linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unuse
linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:49:9-49:10: warning: unused variable `z` [linter.unusedVariables]

2
tests/lean/run/simp1.lean
View file

@ -29,6 +29,8 @@ axiom aux {α} (f : List α → List α) (xs ys : List α) : f (xs ++ ys) ++ []
open Lean
open Lean.Meta
#eval 1 -- TODO: remove, this is a workaround to make sure then next eval works.
def tst1 : MetaM Unit := do
let thms ← Meta.getSimpTheorems
trace[Meta.debug] "{thms.pre}\n-----\n{thms.post}"