lean2/tests/lean/attr_at2.lean.expected.out

sec 3. 
definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
sec 2. 
definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
sec 1. 
definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
foo.bah.bla. 
definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
foo.bah. 
definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
foo. 
definition foo.bah.bla.f : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
root. 
definition foo.bah.bla.f : ℕ → ℕ :=
λ a, a + 1
definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								sec 3.
 								definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								sec 2.
 								definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								sec 1.
 								definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								foo.bah.bla.
 								definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								foo.bah.
 								definition foo.bah.bla.f [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								foo.
 								definition foo.bah.bla.f : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								root.
 								definition foo.bah.bla.f : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + 1
-												feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces

											
										
										
											2015-12-05 18:28:01 +00:00
+								definition foo.bah.bla.g [reducible] : ℕ → ℕ :=
-												chore(tests): mass-update for pp.binder_types false

											
										
										
											2016-06-01 02:14:42 +00:00
+								λ a, a + a