Zulip Chat Archive

Stream: general

Topic: projection notation with {}


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

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