Zulip Chat Archive
Stream: general
Topic: infer_instance'
Kenny Lau (Feb 25 2019 at 10:26):
If I PR this to mathlib, which file should I put it in?
/-- Like `infer_instance`, but works for Sort 0. -/ @[reducible] def infer_instance' {α : Sort u} [i : α] : α := i
Last updated: May 02 2025 at 03:31 UTC