Commit 2025-10-22 16:00 f31d6cc2

View on Github →

chore(Data/Typevec): Move variables into variable declaration in typevec (#27552) This will be needed to allow M.corec to be generic across universes

Estimated changes

Modified Mathlib/Data/TypeVec.lean

modified theorem TypeVec.Arrow.ext

modified def TypeVec.Arrow

modified def TypeVec.comp

modified theorem TypeVec.comp_assoc

modified theorem TypeVec.comp_id

modified theorem TypeVec.id_comp

modified def TypeVec.«repeat»