what is the problem?

Stream: new members

[Michael Werman]

def a: fin 2 → ℝ
 |0 := 1
 |1 := 2

thanks,

[Eric Wieser]

This works:

def foo : fin 2 → ℝ
| ⟨0, _⟩ := 1
| ⟨1, _⟩ := 2
| ⟨n + 2, h⟩ := by linarith

[Eric Wieser]

Perhaps the docs for fin should provide an example of case-matching

[Eric Wieser]

Or the linarith-free version:

def foo : fin 2 → ℝ
| ⟨0, _⟩ := 1
| ⟨1, _⟩ := 2
| ⟨n + 2, h⟩ := false.elim $ n.not_lt_zero $ add_lt_iff_neg_right.mp h
-- or          (not_lt_of_ge (nat.le_add_left 2 n) h).elim

Is there any way to teach the equation compiler to insert this case automatically?

[Yakov Pechersky]

One can define it by sending 0 to 1 and _ (that is, everything else) to 2