lean2/tests/lean/local_notation_bug2.lean

open nat
section
parameters (b : ℕ)
definition add_b (n : ℕ) := n + b
local postfix `%%`:max := add_b
end
eval 5%% -- Error, unexpected token
-												fix(library/scoped_ext): bug in local metadata in sections

The problem is described in issue #554

											
										
										
											2015-04-22 01:56:28 +00:00
+								open nat
 								section
 								parameters (b : ℕ)
 								definition add_b (n : ℕ) := n + b
-												refactor(library/*): use type classes for div and mod

											
										
										
											2015-10-29 19:36:26 +00:00
+								local postfix `%%`:max := add_b
-												fix(library/scoped_ext): bug in local metadata in sections

The problem is described in issue #554

											
										
										
											2015-04-22 01:56:28 +00:00
+								end
-												refactor(library/*): use type classes for div and mod

											
										
										
											2015-10-29 19:36:26 +00:00
+								eval 5%% -- Error, unexpected token