how to force an evaluation of a fuction on a wildcard case

Stream: lean4

[Xiaoning Bian]

The following code won't typecheck in Lean4 (neither in Agda):

def df (n : Nat) : Type :=
  match n with
  | 0 => Bool
  | 1 => Nat
  | 2 => List Bool
  | _ => Unit

def dff (n : Nat) : df n :=
  match n with
  | 0 => true
  | 1 => (1 : Nat)
  | 2 => ([true, false] : List Bool)
  | _ => (() : Unit)

The last line is problematic.

[Henrik Böving]

def df (n : Nat) : Type :=
  match n with
  | 0 => Bool
  | 1 => Nat
  | 2 => List Bool
  | n + 3 => Unit

def dff (n : Nat) : df n :=
  match n with
  | 0 => true
  | 1 => (1 : Nat)
  | 2 => ([true, false] : List Bool)
  | n + 3 => (() : Unit)

write it like this and it works. You can also get your original version to work with some difficulty if you really want. This version gives you better defeq

[Xiaoning Bian]

Thanks! that works. replacing n by _ also works, which is slightly better in having no warning. Thanks for the quick response!

Same solution also works in Agda. uisng (suc (suc (suc _))) instead of _ + 3.