minor refactor to fun_prop fixes #143669
lecopivobuild.yml
on: push
Cancel Previous Runs (CI)
2s
Post-CI job
0s
Annotations
2 errors
|
Build:
Mathlib/CategoryTheory/Monoidal/Opposite.lean#L42
@CategoryTheory.MonoidalOpposite.unmop_inj_iff should not be marked simp
|
|
Build
The process '/usr/bin/env' failed with exit code 1
|