Def expandSuppressCompilationNotation

Modification history

2023-10-11 09:58
Mathlib/Tactic/SuppressCompilation.lean
feat: use suppress_compilation in tensor products (#7504) …
Added expandSuppressCompilationNotationView on Github →