Topic: bug in `@[derive]`?
Kevin Buzzard (Dec 16 2022 at 18:04):
Lean 3 (yeah I know Lean 3 is so early 2022, but I'm trying to get some PRs off the review queue before a possible flag day):
import topology.instances.real example : topological_ring ℝ := infer_instance -- works example : topological_space ℝ := infer_instance -- works @[derive topological_ring] def my_reals := ℝ /- failed to synthesize type class instance for ⊢ topological_space my_reals -/
Should that not be happening?
Last updated: Aug 03 2023 at 10:10 UTC