# Zulip Chat Archive

## Stream: lean4

### Topic: subscript uparrow

#### Jason Gross (Mar 05 2021 at 22:37):

What does the purple subscript uparrow mean? (Apparently it's `\textdied`

in Lean input mode...)

image.png

#### Bryan Gin-ge Chen (Mar 05 2021 at 22:41):

It's a cross: :cross:️. Those indicate names which are inaccessible by the user. See e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Come.20on/near/226307180

#### Jason Gross (Mar 05 2021 at 22:46):

Thanks. The name isn't inaccessible to the user, though, it just doesn't exist in the context where Lean is performing unification, I think...

#### Sebastian Ullrich (Mar 05 2021 at 22:56):

The binding of the motive Gamma was inserted implicitly and is therefore inaccessible. Not sure about the unification error itself, it's too late for that here...

#### Brandon Brown (May 05 2021 at 01:13):

I'm having a similar issue with the cross, trying to prove the following (MWE):

```
inductive int where
| zero : int
| succ : int → int
| pred : int → int
protected def int.norm (a : int) : int :=
match a with
| int.zero => int.zero
| int.succ (int.pred a) => int.norm a
| int.pred (int.succ a) => int.norm a
| int.succ a => int.succ (int.norm a)
| int.pred a => int.pred (int.norm a)
#reduce int.zero |> int.succ |> int.pred |> int.succ |> int.pred |> int.norm
def intn := {x : int // x = (int.norm x)}
example (a : int): int.norm (int.succ a) = int.norm (int.norm (int.succ a)) := by
induction a
rfl
/- Tactic State:
case succ
a✝ : int
v_0✝ : int.norm (int.succ a✝) = int.norm (int.norm (int.succ a✝))
⊢ int.norm (int.succ (int.succ a✝)) = int.norm (int.norm (int.succ (int.succ a✝)))
-/
```

How I am supposed to prove this without having the variables accessible?

#### Brandon Brown (May 05 2021 at 01:27):

(deleted)

#### Sebastian Ullrich (May 05 2021 at 06:33):

See https://raw.githubusercontent.com/IPDSnelting/tba-2021/master/slides/lecture4.pdf#page=26, last slide and preceding slides. You can name them using either induction-with or `case`

(recent nightly).

#### Sebastian Ullrich (May 05 2021 at 06:34):

The alternative we did *not* mention in the course is

```
set_option tactic.hygienic false
```

as well as the `unhygienic`

tactic combinator

Last updated: May 18 2021 at 23:14 UTC