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

chore: fix flaky test

Browse source
This commit is contained in:
Gabriel Ebner 2023-05-15 13:23:38 -07:00
parent 555f5f390c
commit ebc32af2e6
1 changed files with 25 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
tests/lean/1616.lean.expected.out
View file

@ -1,33 +1,13 @@
1616.lean:9:31-9:38: error: don't know how to synthesize implicit argument
@Cover.left ?m ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
@Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
@Cover.right ?m ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
@Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
@Linear ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
@Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:10:12-10:20: error: don't know how to synthesize implicit argument
@Linear ?m ?m ?m ?m c
context:
@ -37,14 +17,34 @@ c : Cover ?m ?m ?m
@Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
@Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
@Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:9:31-9:38: error: don't know how to synthesize implicit argument
@Cover.left ?m ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
@Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
context:
c : Cover ?m ?m ?m
⊢ List ?m
1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
@Cover.right ?m ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
@Linear ?m ?m ?m ?m c
context:
c : Cover ?m ?m ?m
⊢ Type u_1
1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
@Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
context:
c : Cover ?m ?m ?m
⊢ Type u_1