hide implicit arguments from matching

Stream: new members

[kana]

Is there some option, that will allow to not write _ for implicit arguments?

inductive x : bool → Type
| a : x true
| b : x false

def f : ∀{b : bool}, x b → nat
| _ x.a := 0
| _ x.b := 1

or

def y : ∀{A : Type} (x : A), A := λ_ x, x

[Yakov Pechersky]

You could put them to the left of the colon

[Yakov Pechersky]

"def f {b : bool} : x b -> nat | x.a := 0 | x.b := 1"

[Yakov Pechersky]

I think lean 4 also makes different choices about the availability of implicit args in match sections like this

[kana]

I cant move b on left side, because matching of x bdepends on b.

Explicitly it is matching on both args

def f : ∀{b : bool}, x b → nat
| true x.a := 0
| false x.b := 1

[Yakov Pechersky]

Well, for your "y" example, you can

[kana]

Real case is not def, but something like { assoc := \lam _ _ _ _ f g h, ... }

[Eric Wieser]

Why do you want to avoid the _s? If they weren't there, then what would you do if you actually do need to match on them?

[Eric Wieser]

Also, it sounds like your real case isn't a pattern match at all

[kana]

Syntax like { assoc := \lam {_ _ _ _} f g h, ... } also works, so I guess, if implicit args were hidden on lambda arguments, it will possible to bind them to context like this

\lam x, x
\lam {A} x, x

[kana]

So, right now I have such code

inductive X | A | B open X

inductive HomX : X -> X -> Type
| id {x} : HomX x x
| f : HomX A B
| g : HomX B A

namespace HomX
def comp : ∀{a b c}, HomX b c -> HomX a b -> HomX a c
| _ _ _ id x := x
| _ _ _ f id := f
| _ _ _ g id := g
| _ _ _ f g := id
| _ _ _ g f := id
end HomX

And I am wondering, is there a way to write it prettier

[kana]

Oh yes, there is one way

def comp : ∀{a b c}, HomX b c -> HomX a b -> HomX a c :=
  by repeat { rintro ⟨⟩ }; constructor

[Eric Wieser]

You almost certainly don't want that rintro approach as it won't create equation lemmas

[Eric Wieser]

rw comp won't behave nearly as nicely

[Mario Carneiro]

kana said:

Syntax like { assoc := \lam {_ _ _ _} f g h, ... } also works, so I guess, if implicit args were hidden on lambda arguments, it will possible to bind them to context like this

\lam x, x
\lam {A} x, x

What you describe is exactly how implicit lambdas work in lean 4. In lean 3 they are always introduced in lambdas the same as regular arguments

[Mario Carneiro]

My recommendation is to just live with the _'s in your first definition of HomX.comp