## Stream: new members

### Topic: function.app

#### Horatiu Cheval (Apr 12 2021 at 18:41):

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 (Apr 12 2021 at 18:54):

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 (Apr 12 2021 at 19:13):

def app_func (T) := @id T

#### Eric Wieser (Apr 12 2021 at 19:14):

docs#function.app for reference

#### Eric Wieser (Apr 12 2021 at 19:16):

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

#### Eric Wieser (Apr 12 2021 at 19:18):

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

#### Eric Wieser (Apr 12 2021 at 19:20):

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

#### Horatiu Cheval (Apr 12 2021 at 19:36):

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 (Apr 12 2021 at 20:57):

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

Last updated: May 13 2021 at 19:20 UTC