Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Add mathlib4 porting warnings

feat(combinatorics/simple_graph): Locally linear graphs #7374

Sign in to view logs

feat(combinatorics/simple_graph): Locally linear graphs

feat(combinatorics/simple_graph): Locally linear graphs #7374

Triggered via pull request October 23, 2023 07:19
@YaelDilliesYaelDillies
synchronize #19201
locally_linear_graph
Status Success
Total duration 35s
Artifacts –

add_ported_warnings.yml

on: pull_request
Check for modifications to ported files
26s
Check for modifications to ported files
Fit to window
Zoom out
Zoom in

Annotations

2 warnings
Check for modifications to ported files: src/combinatorics/simple_graph/basic.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
Check for modifications to ported files: src/combinatorics/simple_graph/triangle/basic.lean#L1
Changes to this file will need to be ported to mathlib 4! Please consider retracting the changes to this file unless you are willing to immediately forward-port them.