bla : Type
point : Type
point.mk : ℕ → ℕ → point
point.rec : (Π (x y : ℕ), ?M_1 {x := x, y := y}) → Π (n : point), ?M_1 n
point.rec_on : Π (n : point), (Π (x y : ℕ), ?M_1 {x := x, y := y}) → ?M_1 n
point.cases_on : Π (n : point), (Π (x y : ℕ), ?M_1 {x := x, y := y}) → ?M_1 n
point.induction_on : ∀ (n : point), (∀ (x y : ℕ), ?M_1 {x := x, y := y}) → ?M_1 n
point.x : point → ℕ
point.y : point → ℕ
bla : Type
private_structure.lean:24:6: error: unknown identifier 'point'
private_structure.lean:25:6: error: unknown identifier 'point.mk'
private_structure.lean:26:6: error: unknown identifier 'point.rec'
private_structure.lean:27:6: error: unknown identifier 'point.rec_on'
private_structure.lean:28:6: error: unknown identifier 'point.cases_on'
private_structure.lean:29:6: error: unknown identifier 'point.induction_on'
private_structure.lean:30:6: error: unknown identifier 'point.no_confusion'
private_structure.lean:31:6: error: unknown identifier 'point.x'
private_structure.lean:32:6: error: unknown identifier 'point.y'
def foo.bla : Type :=
point
private_structure.lean:37:7: error: invalid constructor ⟨...⟩, type is a private inductive datatype
sorry : foo.bla
foo.mk : foo.bla
