Zulip Chat Archive

Stream: general

Topic: getting notation to work


view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 03 2020 at 15:14):

Is there a way to make this work nonetheless?

view this post on Zulip Yury G. Kudryashov (Jun 04 2020 at 03:37):

Does local notation work?

view this post on Zulip 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