Skip to content
Back to pull request #7906

use abbrev #51303

Sign in to view logs

use abbrev

use abbrev #51303

Triggered via push October 26, 2023 06:49
@FR-vdash-botFR-vdash-bot
pushed 34d3256
FR_ndfunlike
Status Failure
Total duration 4m 10s
Artifacts –
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

build.yml

on: push
Lint style
2m 32s
Lint style
Check all files imported
10s
Check all files imported
Build
4m 1s
Build
Cancel Previous Runs (CI)
5s
Cancel Previous Runs (CI)
check workflows
12s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

10 errors
Build: Mathlib/Data/FunLike/Embedding.lean#L134
'NDFunLike' is not a structure
Build: Mathlib/Data/FunLike/Embedding.lean#L137
Declaration EmbeddingLike not found.
Build: Mathlib/Data/FunLike/Embedding.lean#L141
unknown identifier 'EmbeddingLike'
Build: Mathlib/Data/FunLike/Embedding.lean#L143
unknown identifier 'F'
Build: Mathlib/Data/FunLike/Embedding.lean#L144
unknown identifier 'injective''
Build: Mathlib/Data/FunLike/Embedding.lean#L145
Declaration EmbeddingLike.injective not found.
Build: Mathlib/Data/FunLike/Embedding.lean#L148
unknown identifier 'F'
Build: Mathlib/Data/FunLike/Embedding.lean#L148
unknown identifier 'α'
Build: Mathlib/Data/FunLike/Embedding.lean#L148
unknown identifier 'α'
Build: Mathlib/Data/FunLike/Embedding.lean#L149
unknown identifier 'EmbeddingLike.injective'