Def dummyInst

Modification history

2026-10-05 11:29

MathlibTest/Linter/GlobalAttributeIn.lean

chore(Linter): remove the upstreamed `globalAttributeIn` (#44499) …

Deleted dummyInst View on Github →

2026-05-29 13:23

MathlibTest/globalAttributeIn.lean

chore: bump toolchain to v4.31.0-rc1 (#39980)

Added dummyInst View on Github →