Add TODO (remove multideg\'
)
#6
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
build.yml
on: push
Cancel Previous Runs (CI)
0s
Build
6m 43s
Annotations
2 warnings
Build:
Division.lean#L118
unused variable `hp` [linter.unusedVariables]
|
Build:
Division.lean#L160
unused variable `hp` [linter.unusedVariables]
|