Zulip Chat Archive

Stream: new members

Topic: function.app


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

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

view this post on Zulip Eric Wieser (Apr 12 2021 at 19:13):

def app_func (T) := @id T

view this post on Zulip Eric Wieser (Apr 12 2021 at 19:14):

docs#function.app for reference

view this post on Zulip Eric Wieser (Apr 12 2021 at 19:16):

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

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

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

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

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