This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Updated normal correspondence code to Lean 4 #121024
Annotations
6 errors and 11 warnings
|
src/field_theory/normal_correspondence.lean#L1
ERR_COP: Malformed or missing copyright header
|
|
src/field_theory/normal_correspondence.lean#L2
ERR_COP: Malformed or missing copyright header
|
|
src/field_theory/normal_correspondence.lean#L1
ERR_COP: Malformed or missing copyright header
|
|
src/field_theory/normal_correspondence.lean#L4
ERR_COP: Malformed or missing copyright header
|
|
src/field_theory/normal_correspondence.lean#L4
ERR_MOD: Module docstring missing, or too late
|
|
|
|
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-python@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
src/field_theory/normal_correspondence.lean#L10
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L19
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L23
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L26
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L27
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L35
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L44
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L51
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L52
WRN_BRC: Probable misformatting of curly braces
|
|
src/field_theory/normal_correspondence.lean#L56
WRN_BRC: Probable misformatting of curly braces
|
The logs for this run have expired and are no longer available.
Loading