Best wildcard value for case definition

Stream: general

[Teddy Baker]

I am making a case based definition using match, and in order to compile I have to provide a "wildcard" case which in practice should never appear. Here is the definition

def card_solution : ℕ := 4
noncomputable def solution (n : Fin card_solution) : ℤ → ℝ :=
  match n.val with
  | 0 => fun m => (π / 2 + m * π)
  | 1 => fun m => (π / 4 + m * π / 2)
  | 2 => fun m => (π / 6 + m * π / 6)
  | 3 => fun m => (5 * π / 6 + m * π / 6)
  | _ => fun m => 0

I might prefer for the wildcard to have something like a Nan (not a number) instead of 0. Is there a way to do this? I haven't found an appropriate "error number" within lean to put there.

[Heather Macbeth]

#mwe

[Heather Macbeth]

You could do

import Mathlib
open Real

def card_solution : ℕ := 4
noncomputable def solution (n : Fin card_solution) : ℤ → Option ℝ :=
  match n.val with
  | 0 => fun m => some (π / 2 + m * π)
  | 1 => fun m => some (π / 4 + m * π / 2)
  | 2 => fun m => some (π / 6 + m * π / 6)
  | 3 => fun m => some (5 * π / 6 + m * π / 6)
  | _ => fun m => none

[Vincent Beffara]

Or,

import Mathlib
open Real

def card_solution : ℕ := 4
noncomputable def solution (n : Fin card_solution) : ℤ → ℝ :=
  match n.val with
  | 0 => fun m => (π / 2 + m * π)
  | 1 => fun m => (π / 4 + m * π / 2)
  | 2 => fun m => (π / 6 + m * π / 6)
  | 3 => fun m => (5 * π / 6 + m * π / 6)
  | _ => fun _ => default

(default is 0 here but at least it makes it clearer that the value does not matter.)

[Vincent Beffara]

Actually:

import Mathlib
open Real

abbrev card_solution : ℕ := 4
noncomputable def solution (n : Fin card_solution) : ℤ → ℝ :=
  match n with
  | 0 => fun m => (π / 2 + m * π)
  | 1 => fun m => (π / 4 + m * π / 2)
  | 2 => fun m => (π / 6 + m * π / 6)
  | 3 => fun m => (5 * π / 6 + m * π / 6)

[Jireh Loreaux]

(deleted)

[Vincent Beffara]

No offense taken :-) So what would be your suggestion?

[Jireh Loreaux]

Disregard my previous message. I misread the example.

[Teddy Baker]

Thanks everyone, all of these are very helpful!

[Eric Wieser]

If you are forced to provide a provably impossible case, you can also use False.elim _