| namespace Ex1 | |
| class FunLike (F : Sort _) (β : outParam <| Nat → Sort _) where | |
| coe : F → ∀ a, β a | |
| inductive Secret | |
| def Wrapper := Secret | |
| inductive Bla | z | |
| instance : FunLike Bla (fun _ => Wrapper) := sorry | |
| instance (priority := 100) {F β} [FunLike F β] : | |
| CoeFun F fun _ => ∀ a : Nat, β a where coe := FunLike.coe | |
| #check Bla.z ∘ id | |
| end Ex1 | |
| namespace Ex2 | |
| structure Secret | |
| def Wrapper := Secret | |
| def f (a : Nat) : (fun _ => Wrapper) a := ⟨⟩ | |
| #check f ∘ id | |
| end Ex2 |