Zulip Chat Archive

Stream: new members

Topic: extend projection notation


view this post on Zulip Horatiu Cheval (Apr 05 2021 at 09:08):

Can the x.1 notation for projections be used for other things? I have

inductive type
| zero : type
| arrow : type  type  type
| times : type  type  type

infix `⊗` : 51 := type.times
infixr `↣` : 50 := type.arrow

inductive term : type  Type
| app {σ τ : type} : term (σ  τ)  term σ  term τ
| projl {σ τ : type} : term (σ  τ  σ)
| projr {σ τ : type} : term (σ  τ  τ)

namespace term

def fst {σ τ : type} (x : term $ σ  τ) : term σ :=  app projl x
def snd {σ τ : type} (x : term $ σ  τ) : term τ :=  app projr x

variables {σ τ : type} {x : term $ σ  τ}
#check x.fst

end term

and I'm wondering if I can write x.0 and x.1 for x.fst resp. x.snd


Last updated: May 15 2021 at 00:39 UTC