# Zulip Chat Archive

## Stream: general

### Topic: Pattern match interfering with calc

#### Seul Baek (Mar 13 2019 at 03:15):

I'm currently working with equality elimination, and I frequently use patterns like `(eq::l)`

when equality constraints are encoded as lists. I found that this interferes with the `calc`

enviroment in weird ways. Here's the minimal example I found so far:

lemma foo : ∀ x : list unit, unit | [] := () | (eq::_) := begin have h0 : 0 = 0 := (calc 0 = 0 : rfl ... = 0 : rfl) end invalid occurrence of field notation state: foo : list unit → unit, eq : unit, _x : list unit ⊢ unit

The problem here seems to be that Lean isn't taking `eq`

in the pattern as an arbitrary term of type `unit`

, but as the actual `eq : Π {α : Sort u_1}, α → α → Prop`

(the problem goes away when I rename it to something like `x`

). But this is strange since if Lean considered `eq`

to be the latter, it would usually give a typechecking error and inform you that this `eq`

cannot occur in a list of units. That's precisely what it does when there is, say, a `tt`

in its place.

Last updated: May 11 2021 at 12:15 UTC