def AMSLinter.foo : Nat

Equations

• AMSLinter.foo = 1

theorem AMSLinter.test_theorem : 1 + 1 = 2

A highly non-trivial theorem

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

A highly non-trivial theorem with a helpful hypothesis

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

A highly non-trivial theorem with two helpful hypotheses

theorem AMSLinter.test_lemma : 1 + 1 = 2

theorem AMSLinter.test_theorem_with_docstring : 1 + 1 = 2

A highly non-trivial theorem with a helpful hypothesis

@[simp]

theorem AMSLinter.test_1 : 1 + 1 = 2

@[simp]

theorem AMSLinter.test_3 : 1 + 1 = 2

theorem AMSLinter.test_out_of_order : 1 + 1 = 2

theorem AMSLinter.test_dup : 1 + 1 = 2