beta expand if needed #63554
Annotations
9 errors
|
build mathlib:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1165
application type mismatch
|
|
build mathlib:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1388
typeclass instance problem is stuck, it is often due to metavariables
|
|
build mathlib:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1391
no goals to be solved
|
|
build mathlib:
Mathlib/Computability/AkraBazzi/AkraBazzi.lean#L1292
application type mismatch
|
|
build mathlib:
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:
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:
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:
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 mathlib
The process '/usr/bin/bash' failed with exit code 1
|
The logs for this run have expired and are no longer available.
Loading