lean icon indicating copy to clipboard operation
lean copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(data/int/*): delete int

Open YaelDillies opened this issue 4 years ago • 6 comments

It will be restored on the mathlib on the next release.

YaelDillies avatar Oct 15 '21 11:10 YaelDillies

bors try

YaelDillies avatar Oct 15 '21 11:10 YaelDillies

:lock: Permission denied

Existing reviewers: click here to make YaelDillies a reviewer

bors[bot] avatar Oct 15 '21 11:10 bors[bot]

bors try

gebner avatar Oct 15 '21 11:10 gebner

try

Build failed:

bors[bot] avatar Oct 15 '21 12:10 bors[bot]

bors try

bryangingechen avatar Oct 15 '21 13:10 bryangingechen

try

Build failed:

bors[bot] avatar Oct 15 '21 13:10 bors[bot]