def CategoryLinter.foo : Nat

Equations

• CategoryLinter.foo = 1

theorem CategoryLinter.test_theorem : 1 + 1 = 2

A highly non-trivial theorem

theorem CategoryLinter.test_theorem_with_hypothesis : True → 1 + 1 = 2

A highly non-trivial theorem with a helpful hypothesis

theorem CategoryLinter.test_theorem_with_hypotheses : True → False → 1 + 1 = 2

A highly non-trivial theorem with two helpful hypotheses

theorem CategoryLinter.test_lemma : 1 + 1 = 2

theorem CategoryLinter.test_theorem_with_docstring : 1 + 1 = 2

A highly non-trivial theorem with a helpful hypothesis

theorem CategoryLinter.test_2 : 1 + 1 = 2

@[simp]

theorem CategoryLinter.test_1 : 1 + 1 = 2

@[simp]

theorem CategoryLinter.test_3 : 1 + 1 = 2