Default pattern with nested inductive

Stream: lean4

[Horațiu Cheval]

I have the inductive type Proof whose constructor nested takes a term of another inductive type (Context).
When pattern-matching on prf : Proof t in the definition of isAny the default pattern | _ => false does not work as expected (i.e. dealing with the case nested). In general it seems that if more constructors are present, all the nested ones are ignored by _.

inductive Term
| application : Term → Term → Term

open Term

inductive Context
| mk : Term → Context

def Context.insert (t : Term) : Context → Term
| .mk u => application u t

inductive Proof  : Term → Type
| any (t) : Proof t
| nested (C : Context) (t : Term) : Proof (C.insert t)

def isAny (t) (prf : Proof t) : Bool :=
match prf with
| .any _ => true
| _ => false

The error I get at match is

  missing cases:
  (Proof.nested(Context.mk _) _)

and also redundant alternative at |_ => false. Is there a way I can make this work?

[James Gallicchio]

(deleted)

[James Gallicchio]

(deleted)

[Henrik Böving]

I'd say this is a bug, the code you wrote should be valid

[Gabriel Ebner]

This works for me with the current nightly.

[Horațiu Cheval]

Yes, it works for me too after updating. Sorry for the noise.