lean2/tests/lean/438.lean

import algebra.bundled
open algebra

attribute Group.struct [coercion]

section
  parameters {P₀ : Type} [P : group P₀]
  include P

  structure lambda_morphism := (comm : _ = _)

end
refactor(library/algebra): move bundled structures to separate module Motivation: performance. After this commit, the bundled instances do not participate in the class/instance resolution if we do not import algebra.bundled. 2015-03-03 02:45:08 +00:00			`import algebra.bundled`
fix(frontends/lean/structure_cmd): effect of "include" command in the structure command closes #438 2015-02-20 06:43:28 +00:00			`open algebra`

			`attribute Group.struct [coercion]`

			`section`
			`parameters {P₀ : Type} [P : group P₀]`
			`include P`

			`structure lambda_morphism := (comm : _ = _)`

			`end`