This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
fix #121022
Annotations
2 errors and 1 warning
src/analysis/normed_space/star/exponential.lean#L36
/home/lean/actions-runner/_work/mathlib/mathlib/src/analysis/normed_space/star/exponential.lean:36:1:
none of the overloads are applicable
error for exp
function expected at
exp ℂ
term has type
Type
error for complex.exp
failed to synthesize type class instance for
A : Type u_1,
_inst_1 : normed_ring A,
_inst_2 : normed_algebra ℂ A,
_inst_3 : star_ring A,
_inst_4 : has_continuous_star A,
_inst_5 : complete_space A,
_inst_6 : star_module ℂ A,
a : ↥(self_adjoint A)
⊢ has_smul ℂ ↥(self_adjoint A)
Additional information:
/home/lean/actions-runner/_work/mathlib/mathlib/src/analysis/normed_space/star/exponential.lean:36:1: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type, because failed to elaborate all candidates using the expected type
A
this can happen because, for example, coercions were not considered in the process
none of the overloads are applicable
error for exp
too many arguments
error for complex.exp
too many arguments
|
|
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
The logs for this run have expired and are no longer available.
Loading