lean2/tests/lean/run/585.lean

import data.finset.basic

open finset

check ∅                 -- o.k.
check λs t, subset s t  -- o.k.
check λs t, s ⊆ t       -- fixed

infix `⊆` := subset
check λs t, s ⊆ t
fix(frontends/lean/notation_cmd): fixes #585 2015-05-07 15:35:46 +00:00			`import data.finset.basic`

			`open finset`

			`check ∅ -- o.k.`
			`check λs t, subset s t -- o.k.`
			`check λs t, s ⊆ t -- fixed`

refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function 2015-05-23 06:16:36 +00:00			infix `⊆` := subset
fix(frontends/lean/notation_cmd): fixes #585 2015-05-07 15:35:46 +00:00			`check λs t, s ⊆ t`