15 lines
262 B
Text
15 lines
262 B
Text
A.x : Nat
|
|
B.y : Nat
|
|
A.x : Nat
|
|
A.x : Nat
|
|
B.y : Nat
|
|
openExport.lean:19:7: error: unknown identifier 'x'
|
|
(sorryAx ?m.44) : ?m.44
|
|
openExport.lean:20:7: error: unknown identifier 'y'
|
|
(sorryAx ?m.46) : ?m.46
|
|
A.x : Nat
|
|
B.y : Nat
|
|
A.x : Nat
|
|
B.y : Nat
|
|
B.z : Nat
|
|
B.z : Nat
|