## Stream: new members

### Topic: problems with equation compiler & subsets

#### Nicolas Rouquette (Nov 08 2020 at 05:38):

I am trying to define a function where the domain is a subset of elements and I'm really surprised at Lean's behavior.
Can someone please explain how to define a function using the equation compiler for a subset type ?

import data.fintype.basic

def ns := {n: ℕ | n ≤ 3}

def n0 : ns := ⟨ 0, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n1 : ns := ⟨ 1, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n2 : ns := ⟨ 2, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n3 : ns := ⟨ 3, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩

def n2s_incomplete : ns → string
| n0 := "zero"

#eval n2s_incomplete n1
-- result: "zero"  -- why is this the case?

#eval n2s_incomplete n0
-- result: "zero" -- this function seems to be equivalent to a constant; that is, the argument seems to be completely ignored.

def n2s : ns → string
| n0 := "0" -- no error
| n1 := "1" -- equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
| n2 := "2" -- equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
| n3 := "3" -- equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable


#### Alex J. Best (Nov 08 2020 at 06:38):

lean is treating n0 on the left as just a new identifier. Doing

def n2s_incomplete : ns → string
| ⟨0, h⟩ := "zero"
| ⟨1, h⟩ := "one"
| ⟨2, h⟩ := "two"
| ⟨3, h⟩ := "three"
| ⟨n + 4, h⟩ := ""


seems to work. There is an attribute @[pattern] you can add to defs, but lean doesn't like it in this case.

#### Alex J. Best (Nov 08 2020 at 06:39):

But if you really just want a type with four terms you can just make a simple inductive

inductive ns
| n0
| n1
| n2
| n3

open ns
def n2s : ns → string
| n0 := "0"
| n1 := "1"
| n2 := "2"
| n3 := "3"


#### Nicolas Rouquette (Nov 08 2020 at 17:56):

Alex J. Best said:

lean is treating n0 on the left as just a new identifier. Doing

def n2s_incomplete : ns → string
| ⟨0, h⟩ := "zero"
| ⟨1, h⟩ := "one"
| ⟨2, h⟩ := "two"
| ⟨3, h⟩ := "three"
| ⟨n + 4, h⟩ := ""


seems to work. There is an attribute @[pattern] you can add to defs, but lean doesn't like it in this case.

Thanks Alex!

Last updated: Dec 20 2023 at 11:08 UTC