Zulip Chat Archive

Stream: new members

Topic: hide implicit arguments from matching


kana (Jun 27 2021 at 12:07):

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 (Jun 27 2021 at 12:09):

You could put them to the left of the colon

Yakov Pechersky (Jun 27 2021 at 12:10):

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

Yakov Pechersky (Jun 27 2021 at 12:12):

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

kana (Jun 27 2021 at 12:15):

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 (Jun 27 2021 at 12:26):

Well, for your "y" example, you can

kana (Jun 27 2021 at 12:43):

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

Eric Wieser (Jun 27 2021 at 12:44):

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 (Jun 27 2021 at 12:44):

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

kana (Jun 27 2021 at 12:46):

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 (Jun 27 2021 at 12:49):

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 (Jun 27 2021 at 12:50):

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 (Jun 27 2021 at 12:51):

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

Eric Wieser (Jun 27 2021 at 12:51):

rw comp won't behave nearly as nicely

Mario Carneiro (Jun 28 2021 at 15:24):

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 (Jun 28 2021 at 15:25):

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


Last updated: Dec 20 2023 at 11:08 UTC