Check for modules that should use `prelude`

chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas #5952

Sign in to view logs

Triggered via pull request November 6, 2024 23:14

kim-em

synchronize #5969

upstream_insertIdx

Status Success

Total duration 14s

Artifacts –

check-prelude.yml

on: pull_request