Implicit arguments after explicit ones

Stream: new members

[nrs]

ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
ƛ′_⇒_ (` x) N = ƛ x ⇒ N

The above is a function in Agda, but so far in Lean I've only encountered implicits coming before explicit arguments. Would there be a way to implement a similar function in Lean (or, in general, how do you use implicit arguments after explicits ones in Lean)?

[Edward van de Meent]

i don't know Agda, so i'm having a hard time decoding what the snippet you give does, but you certainly can "mix & match" implicit and explicit arguments in lean.

[Edward van de Meent]

even if you just look at docs#id , you can see that an implicit argument precedes an explicit one.

[nrs]

Edward van de Meent said:

i don't know agda, so i'm having a hard time decoding what the snippet you give does, but you certainly can "mix'n match" implicit and explicit arguments in lean.

The function is ensuring that t satisfies T (var? t), and thanks for the answer! I'll try to find some examples. Wrt. docs#id, yeah so far I've only found implicit arguments preceding explicit ones

[nrs]

ah I've found some as you said! thanks for the link

[Notification Bot]

nrs has marked this topic as resolved.

[Notification Bot]

nrs has marked this topic as unresolved.

[nrs]

This is how to implement the above function in Lean, if it is of interest to anyone:

def newLambda (t : Term) {_ : T (var? t)} (tt: Term) : Term :=
  match t, tt with
  | !!t, tt => ƛ t tt

[Edward van de Meent]

i'm afraid that doesn't compile...

[Edward van de Meent]

what is T (var? t) supposed to mean? because that isn't valid lean syntax... i see i didn't read your messages

[Edward van de Meent]

i expect that there also is some context missing

[nrs]

Edward van de Meent said:

i'm afraid that doesn't compile...

oh very sorry, forgot to add the context: https://plfa.github.io/Lambda/, it's an implementation of lambda calculus in Agda. The function T is given by def T (b : Bool) : Type := if b = True then Unit else Empty

[nrs]

i also realized I didn't need to match tt in the statement