FormalConjecturesTest/Util/Linters/NamespaceLinter.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem Foo.test_in_namespace line 26 source
2. def Foo.test_def line 30 source
3. theorem Bar.Baz.test_nested_namespace line 38 source
4. theorem test_no_namespace line 50 source
5. def test_def_no_namespace line 59 source
6. theorem test_disabled line 64 source