blob: 7f892bad56df7e6b737eecc906154327d9f3910e [file] [edit]
@[reducible] protected def A.b : A → Nat :=
fun self => self.2
@[reducible] private def A.c : A → Nat :=
fun self => self.3
@[reducible] private def C.d : C → Nat :=
fun self => self.2
@[reducible] protected def C.e : C → Nat :=
fun self => self.3