feat: shrink Has/Preserves/Reflects via UnivLE #56514
Annotations
10 errors
build mathlib:
Mathlib/CategoryTheory/Limits/Yoneda.lean#L165
Declaration Set.range is not allowed to exist in this file
|
build mathlib:
Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean#L104
unknown identifier 'hasColimitsOfSize_shrink'
|
build mathlib:
Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean#L106
failed to synthesize instance
|
build mathlib:
Mathlib/CategoryTheory/Sites/Grothendieck.lean#L309
application type mismatch
|
build mathlib:
Mathlib/CategoryTheory/Sites/Grothendieck.lean#L309
failed to synthesize
|
build mathlib:
Mathlib/CategoryTheory/Sites/Grothendieck.lean#L304
stuck at solving universe constraint
|
build mathlib:
Mathlib/CategoryTheory/Sites/Grothendieck.lean#L293
stuck at solving universe constraint
|
|
|
|
The logs for this run have expired and are no longer available.
Loading