## Stream: general

### Topic: getting notation to work

#### Johan Commelin (Jun 03 2020 at 15:14):

I'm trying to use notation to hide a "parameter": an explicit variable that is constant in the entire file.
But it isn't working. Here is a MWE.

import algebra.big_operators -- should be sufficient

def foo (n : ℕ) (X : Type) [has_pow X ℕ] : X → X := λ x, x^n

variables (p : ℕ) (X : Type) [has_pow X ℕ]

localized "notation bar := foo p" in xyzzy

open_locale xyzzy

example : bar X = bar X :=
begin
-- goal state shows foo p X instead of bar X
end


#### Johan Commelin (Jun 03 2020 at 15:14):

Is there a way to make this work nonetheless?

#### Yury G. Kudryashov (Jun 04 2020 at 03:37):

Does local notation work?

#### Johan Commelin (Jun 04 2020 at 04:48):

Same problem:

def foo (n : ℕ) (X : Type) [has_pow X ℕ] : X → X := λ x, x^n

variables (p : ℕ) (X : Type) [has_pow X ℕ]

local notation bar := foo p

example : bar X = bar X :=
begin
-- goal state shows foo p X instead of bar X
end


Last updated: May 13 2021 at 18:26 UTC