# Zulip Chat Archive

## Stream: general

### Topic: prettyprinter and parameters

#### Kevin Buzzard (Apr 28 2020 at 11:58):

"Let $G$ be a group, let $H$ be a subgroup. Define an equivalence relation $\sim$ on $G$ by $a\sim b\iff ab^{-1}\in H$. Now let's prove some trivial things".

I am trying to set this up in Lean, ideally using `~`

for the equivalence relation because it's what mathematicians are used to. The problem is that the notation depends on H, which can't be inferred, so I need to use `H : subgroup G`

as a parameter, which seems to force me to have `G`

as a parameter as well. Here are two attempts, the first makes notation leak and the second is hilarious :-)

Is there any way I can use notation which depends on a variable or parameter, and get Lean to behave itself?

Aah -- making H implicit as well seems to solve the problem. My instinct is that this might cause me problems later but at least it's a workaround.

```
/-
Let G be a group and let H be a subgroup. Define an equivalence relation ~ by a ~ b ↔ ab⁻¹ ∈ H. This equivalence relation is reflexive.
-/
structure subgroup (G : Type) [group G] :=
(carrier : set G)
/-
axioms omitted
-/
instance (G : Type) [group G] : has_mem G (subgroup G) := ⟨λ m H, m ∈ H.carrier⟩
section rel1
parameters (G : Type) [group G] (H : subgroup G) -- note (G)
def rel1 : ∀ (a b : G), Prop := λ a b, a * b⁻¹ ∈ H
local notation a ` ~ ` b := rel1 a b -- needs to be local because it depends on H
example : ∀ (a : G), a ~ a :=
begin
-- ⊢ ∀ (a : G), rel1 a a -- notation was not kept
sorry
end
end rel1
section rel2
parameters {G : Type} [group G] (H : subgroup G) -- implicit {G}
def rel2 : ∀ (a b : G), Prop := λ a b, a * b⁻¹ ∈ H
local notation a ` ~~ ` b := rel2 a b
example : ∀ (a : G), a ~~ a :=
begin
-- ⊢ ∀ (a : G), (H ~~ a) a -- wtf??
sorry
end
end rel2
```

Last updated: May 10 2021 at 00:31 UTC