function.app

Stream: new members

[Horatiu Cheval]

This doesn't typecheck and I don't really get why:

example (x : {n : ℤ // 0 ≤ n}) := function.app subtype.val x

It works if instead I define my own non-dependent version of function.app

def function.app' {α : Sort u} {β : Sort v} (f : α → β) (a : α) : β := f a
example (x : {n : ℤ // 0 ≤ n}) := function.app' subtype.val x

and then with subtype.property it's the other way around: it works with app but of course not with app'.

How do I write a function app_func such that any application f x may be written as app_func f x?

[Horatiu Cheval]

And for context, maybe I should've asked this first, I was always bothered by the fact that $ doesn't work in tactic mode without outer parentheses, and I was trying to define using function.app an infix notation like $ but with a different precedence, so that it would work in tactic mode. Does something along these lines already exist?

[Eric Wieser]

def app_func (T) := @id T

[Eric Wieser]

docs#function.app for reference

[Eric Wieser]

Woah, there's some weird notation right next to src#function.app

[Eric Wieser]

(+) -[(*)]- (-) is the function that computes the difference of the squares of its arguments (in a commutative ring)

[Eric Wieser]

While ((+) on list.length) is the function that adds the lengths of it's two list arguments

[Horatiu Cheval]

I didn't realize I could think of id as a function of two argument, thanks, that's much more elegant than what I was trying.
Now I can have infixr $$ : 10 := id and I can write things like let y := h $$ g $$ f x, in tactic mode, it's great.

[Yury G. Kudryashov]

on is used, e.g., in pairwise ((≠) on f)