## Stream: general

### Topic: projection notation with {}

#### Kevin Buzzard (Mar 24 2019 at 19:20):

def P : ℕ → Prop := sorry

-- imagine this is in core so I can't change the {} choice
structure bar (α : Type*) :=
(h : ∀ {x : ℕ}, P x)

-- This is my cool structure
structure foo (α : Type*) :=
(n : ℕ)

-- This is my cool map from my structure to the core one
def foo.to_bar {α : Type*} (f : foo α) : bar α := sorry

-- So now, given a term of type foo α I can make a term of type bar α
-- and hence deduce P x for all x : ℕ

example {α : Type*} (f : foo α) : P 3 :=
--f.to_bar.h -- type mismatch
--f.to_bar.h 3 -- function expected
-- @(f.to_bar.h) 3 -- syntax error
bar.h f.to_bar -- works
`

Do I have to give up on projection notation in situations like this, or is there a clever way to insert the @? I couldn't figure it out.

#### Floris van Doorn (Mar 25 2019 at 19:19):

I think you have to give up on projection notation in this case. I have also noticed this annoying behavior sometimes.

Last updated: May 14 2021 at 06:16 UTC