lean2/tests/lean/bad_class.lean

import logic
namespace foo
definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
attribute subsingleton [class]

protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
λa b, !proof_irrel
end foo
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228 2014-10-07 18:02:15 -07:00			`import logic`
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests 2014-10-08 23:44:09 -07:00			`namespace foo`
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228 2014-10-07 18:02:15 -07:00			`definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b`
refactor(frontends/lean): add 'attribute' command The new command provides a uniform way to set declaration attributes. It replaces the commands: class, instance, coercion, multiple_instances, reducible, irreducible 2015-01-24 20:23:21 -08:00			`attribute subsingleton [class]`
feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228 2014-10-07 18:02:15 -07:00
			`protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=`
			`λa b, !proof_irrel`
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests 2014-10-08 23:44:09 -07:00			`end foo`