auto_param and bundled functions

Stream: general

[Johan Commelin]

Can this be made to work?

import data.int.cast

def foo (n : ℕ) (hn : 0 < n . tactic.assumption) : ℤ →+* ℤ :=
int.cast_ring_hom _

-- does not work
lemma foo_apply (n : ℕ) (hn : 0 < n) (m : ℤ) : foo n m = m := sorry
-- I don't want to write `foo n hn m`

[Johan Commelin]

(Of course this is a toy example...)

[Johan Commelin]

Somehow I want to tell Lean that it should always try to work out hn by itself. Unless I write @foo

[Johan Commelin]

This might be related to the fact that you can't write {hn : 0 < n . tactic.assumption} with {}-implicit binders. And again, this means that hn will show up in the goal view, whereas I wouldn't mind if it is hidden there as well.

[Riccardo Brasca]

Writing . tactic in an hypothesis means "try to find it by yourself using tactic"?

[Johan Commelin]

Yes

[Johan Commelin]

@Gabriel Ebner do you think that this is something that could be supported in Lean 3? Or is it a huge change/bad idea?

[Gabriel Ebner]

It's possible to support it. It's not too hard (add something with mk_auto_param maybe in post_process_implicit_arg). But you'll probably need to find somebody else to do it.

[Johan Commelin]

Ok, thanks for the info!