doc: add/edit some FLT docstrings (#8910) #5640
mathlib-bors[bot]bors.yml
on: push
Cancel Previous Runs (CI)
4s
check workflows
9s
Post-CI job
0s
Annotations
5 errors and 2 warnings
|
Build:
Mathlib/Data/Set/Basic.lean#L1182
elaboration function for 'Std.ExtendedBinder.«termSatisfies_binder_pred%__»' has not been implemented
|
|
Build:
Mathlib/Data/Set/Basic.lean#L1184
aesop: exceeded maximum number of normalisation iterations (100). This means normalisation probably got stuck in an infinite loop.
|
|
Build:
Mathlib/Data/Set/Basic.lean#L1189
Declaration Set.ssubset_insert not found.
|
|
Build:
Mathlib/Data/Set/Basic.lean#L1637
unsolved goals
|
|
Build
The process '/usr/bin/bash' failed with exit code 1
|
|
Build:
Mathlib/Data/Set/Basic.lean#L1638
declaration uses 'sorry'
|
|
Build:
Mathlib/Data/Set/Basic.lean#L1638
aesop: failed to prove the goal after exhaustive search.
|