How to recover implicit arguments of inductive types in a match expression?

Question

def IsEven: Nat → Prop
| Nat.zero => True
| Nat.succ pred => ¬IsEven pred

inductive Example: Nat → Prop
| IsExample: IsEven n → Example (n + 10)

Here, IsExample has an implicit parameter n. Let's say I have a value of type Example m, and in order to use it in a proof, I need to refer to the n. How can I do that?

def sillyExampleFunction
  (e: Example m)
:
  IsEven m
:=
  match e with
  | Example.IsExample isEven =>
    -- How may I access the value of `n` here?
    sorry

---

For implicit function parameters, this is possible with function literals by putting the implicit parameters inside curly braces:

def IsMonotonic
  (fn: Nat → Nat)
:=
  -- `n0` and `n1` are implicit parameters.
  ∀ {n0 n1: Nat}, n0 ≤ n1 → fn n0 ≤ fn n1

def doubleIsMono:
  IsMonotonic (fun n => 2 * n)
:=
  fun {n0 n1} le =>
    -- Here we may use `n0` and `n1` in our proof.
    sorry

I've tried matching with

  | Example.IsExample {n} isEven => sorry

but I'm getting the error "too many arguments".

Answer 1

In Lean @foo is like foo but with all arguments made explicit, see documentation on implicit arguments (search for @). To pattern-match against implicit arguments, use the @foo variant, as in this simple example:

inductive Cow : Type
| moo : ∀ {k : Nat}, k = 42 → Cow

-- moo has an implicit argument k

def milk : Cow → Prop
| @Cow.moo k p => (p = p) ∧ (k = k)