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-06-01 06:36:25 -07:00
parent 9102f8cb13
commit bf0b675ca6
14 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/1163.lean.expected.out
View file

@ -1,2 +1,7 @@
1163.lean:6:8-6:15: warning: declaration uses 'sorry'
1163.lean:11:8-11:15: warning: declaration uses 'sorry'
1163.lean:13:16-13:17: error: failed to synthesize instance
OfNat Bool 0
1163.lean:15:8-15:15: warning: declaration uses 'sorry'
1163.lean:18:18-18:19: error: failed to synthesize instance
OfNat Bool 0

1
tests/lean/301.lean.expected.out
View file

@ -1,3 +1,4 @@
301.lean:1:9-1:17: warning: declaration uses 'sorry'
301.lean:1:9-1:17: error: missing cases:
(Nat.succ _)
301.lean:1:21-1:24: error: type mismatch

1
tests/lean/690.lean.expected.out
View file

@ -1,5 +1,4 @@
690.lean:3:2-3:29: error: too many variable names provided at alternative 'step', #3 provided, but #2 expected
690.lean:1:0-1:7: warning: declaration uses 'sorry'
690.lean:6:0-6:7: warning: declaration uses 'sorry'
case step
a b m✝ : Nat

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

@ -2,14 +2,12 @@ myid 10 : Nat
myid true : Bool
autoBoundImplicits1.lean:16:4-16:11: warning: declaration uses 'sorry'
autoBoundImplicits1.lean:20:25-20:29: error: unknown identifier 'size'
autoBoundImplicits1.lean:20:4-20:12: warning: declaration uses 'sorry'
autoBoundImplicits1.lean:24:23-24:24: error: unknown identifier 'α'
autoBoundImplicits1.lean:24:25-24:26: error: unknown identifier 'n'
autoBoundImplicits1.lean:24:33-24:34: error: unknown identifier 'α'
autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β'
autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
autoBoundImplicits1.lean:24:4-24:12: warning: declaration uses 'sorry'
@f : {α : Type} → {n : Nat} → Vec α n → Vec α n
f mkVec : Vec ?m 0
f mkVec : Vec Nat 0

1
tests/lean/bintreeGoal.lean.expected.out
View file

@ -17,4 +17,3 @@ ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
: BST right
: ForallTree (fun k v => key < k) right
⊢ BST left
bintreeGoal.lean:60:8-60:27: warning: declaration uses 'sorry'

1
tests/lean/doLetLoop.lean.expected.out
View file

@ -1 +1,2 @@
doLetLoop.lean:4:0: error: unexpected end of input
doLetLoop.lean:2:4-2:5: warning: declaration uses 'sorry'

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

@ -1 +1,3 @@
doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v'
doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry'
doSeqRightIssue.lean:7:8-7:10: warning: declaration uses 'sorry'

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

@ -28,6 +28,4 @@ inductionErrors.lean:55:2-55:16: error: alternative 'cons' is not needed
inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2'
inductionErrors.lean:66:2-66:28: error: invalid occurrence of wildcard alternative, it must be the last alternative
inductionErrors.lean:74:2-74:34: error: unused alternative
inductionErrors.lean:69:8-69:12: warning: declaration uses 'sorry'
inductionErrors.lean:80:2-80:53: error: unused alternative
inductionErrors.lean:76:8-76:12: warning: declaration uses 'sorry'

1
tests/lean/matchErrorMsg.lean.expected.out
View file

@ -1,2 +1,3 @@
matchErrorMsg.lean:2:1-4:16: warning: declaration uses 'sorry'
matchErrorMsg.lean:2:1-2:6: error: missing cases:
(Prod.mk Nat.zero (Nat.succ _))

1
tests/lean/matchMissingCasesAsStuckError.lean.expected.out
View file

@ -1,2 +1,3 @@
matchMissingCasesAsStuckError.lean:2:2-3:24: warning: declaration uses 'sorry'
matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
none

1
tests/lean/matchUnknownFVarBug.lean.expected.out
View file

@ -1,3 +1,4 @@
matchUnknownFVarBug.lean:2:2-3:19: warning: declaration uses 'sorry'
matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
(some (Nat.succ _)), (some _)
(some (Nat.succ _)), none

1
tests/lean/patvar.lean.expected.out
View file

@ -1,3 +1,4 @@
patvar.lean:3:0-3:22: warning: declaration uses 'sorry'
patvar.lean:3:0-3:22: error: missing cases:
(List.cons _ _)
patvar.lean:10:0-10:16: error: missing cases:

5
tests/lean/substBadMotive.lean.expected.out
View file

@ -1,9 +1,4 @@
substBadMotive.lean:7:4-7:16: warning: declaration uses 'sorry'
substBadMotive.lean:9:23-9:44: error: invalid `▸` notation, failed to compute motive for the substitution
substBadMotive.lean:15:22-15:43: error: invalid `▸` notation, failed to compute motive for the substitution
substBadMotive.lean:13:4-13:15: warning: declaration uses 'sorry'
substBadMotive.lean:13:4-13:15: warning: declaration uses 'sorry'
substBadMotive.lean:34:30-34:53: error: invalid `▸` notation, failed to compute motive for the substitution
substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'
substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'
substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'

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

@ -1,4 +1,2 @@
tooManyVarsAtInduction.lean:3:2-3:31: error: too many variable names provided at alternative 'succ', #4 provided, but #2 expected
tooManyVarsAtInduction.lean:1:8-1:11: warning: declaration uses 'sorry'
tooManyVarsAtInduction.lean:8:2-8:22: error: too many variable names provided at alternative 'succ', #2 provided, but #1 expected
tooManyVarsAtInduction.lean:6:8-6:11: warning: declaration uses 'sorry'