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

chore: fix tests output

Browse source
This commit is contained in:
Leonardo de Moura 2023-10-21 06:47:23 -07:00 • committed by Leonardo de Moura
parent 370476cc14
commit 0bd15be1a1
3 changed files with 57 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,8 +1,3 @@
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:24-10:41: error: don't know how to synthesize implicit argument
@Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
context:
@ -13,33 +8,28 @@ c : Cover ?m ?m ?m
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: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: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: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
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:11-9:19: error: don't know how to synthesize implicit argument
@Linear ?m ?m ?m ?m c
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
@ -48,3 +38,13 @@ c : Cover ?m ?m ?m
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: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

58
tests/lean/jason1.lean.expected.out
View file

@ -1,3 +1,31 @@
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
@ -48,21 +76,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
@ -108,17 +122,3 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G

18
tests/lean/syntheticHolesAsPatterns.lean.expected.out
View file

@ -1,11 +1,3 @@
syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
context:
α✝ β : Type
a✝ : α✝
x : Fam2 α✝ β
α : Type
a : α
⊢ α
syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder
context:
α β : Type
@ -13,9 +5,10 @@ a✝ : α
x : Fam2 α β
a n : Nat
⊢ Nat
syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder
context:
α✝ β : Type
a✝ : α✝
x : Fam2 α✝ β
α : Type
a : α
@ -26,3 +19,10 @@ context:
x : Fam2 α β
n a : Nat
⊢ Nat
syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
context:
α✝ β : Type
x : Fam2 α✝ β
α : Type
a : α
⊢ α