Def TypeVec.«repeat»

Modification history

2025-10-22 16:00

Mathlib/Data/TypeVec.lean

chore(Data/Typevec): Move variables into `variable` declaration in typevec (#27552) …

Modified TypeVec.«repeat»View on Github →

2023-01-17 19:22

Mathlib/Data/TypeVec.lean

feat: port Data.Typevec (#891) …

Added TypeVec.«repeat»View on Github →