lean2/tests/lean/notation4.lean.expected.out

notation4.lean:2:0: warning: imported file uses 'sorry'
∃ (A : Type₁) (x y : A), x = y : Prop
∃ (x : num), x = 0 : Prop
Σ (x : num), x = 10 : Type₁
Σ (A : Type₁), list A : Type₂
feat(frontends/lean/pp): support scopedexpr notation in the pretty printer 2014-10-19 19:48:34 +00:00			`notation4.lean:2:0: warning: imported file uses 'sorry'`
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation 2014-10-19 20:08:15 +00:00			`∃ (A : Type₁) (x y : A), x = y : Prop`
			`∃ (x : num), x = 0 : Prop`
			`Σ (x : num), x = 10 : Type₁`
			`Σ (A : Type₁), list A : Type₂`