Commit 2023-10-03 11:52 363a0f74

feat: new tactic suppress_compilation, use it in OperatorNorm (#7326) The tactic suppress_compilation makes sure that def and instance are replaced by noncomputable def and noncomputable instance so that the compiler does not try to produce executable code. This leads to gains in compilation time and olean sizes. Using it in OperatorNorm.lean reduces the olean size from 10756 kB to 6626 kB, for instance. Implementation due to @tydeu, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/noncomputability.20and.20oleans/near/392451565