beta expand if needed #63554
alexjbestbuild.yml
on: push
Cancel Previous Runs (CI)
3s
check workflows
7s
Post-CI job
0s
Annotations
9 errors
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1165
application type mismatch
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1388
typeclass instance problem is stuck, it is often due to metavariables
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1391
no goals to be solved
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1292
application type mismatch
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1439
invalid field 'T_isBigO_smoothingFn_mul_asympBound', the environment does not contain 'AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound'
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1458
invalid field 'smoothingFn_mul_asympBound_isBigO_T', the environment does not contain 'AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T'
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1462
invalid field notation, function 'AkraBazziRecurrence.isBigO_asympBound' does not have argument with type (AkraBazziRecurrence ...) that can be used, it must be explicit or implicit with a unique name
|
|
Build:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1462
invalid field notation, function 'AkraBazziRecurrence.isBigO_symm_asympBound' does not have argument with type (AkraBazziRecurrence ...) that can be used, it must be explicit or implicit with a unique name
|
|
Build
The process '/usr/bin/bash' failed with exit code 1
|