## Stream: new members

### Topic: Reducing functions that return types

#### Kevin Sullivan (Oct 18 2020 at 18:17):

YEP below works. NOPE doesn't. Where exactly does the latter fail? Beginner question.

inductive foo : Type
| R
| N

def typeForFoo : foo → Type
| foo.R := ℝ
| foo.N := ℕ

-- YEP!
def r : (typeForFoo foo.R) := (1.0 : ℝ)
def n : (typeForFoo foo.N) := (1 : ℕ)

structure bar := mk :: (r : ℝ) (n : ℕ)

-- NOPE!
def jack (f : foo) (s : typeForFoo f) : bar :=
match f with
| foo.R := bar.mk s 0
| foo.N := bar.mk 0 s
end


#### Kevin Sullivan (Oct 18 2020 at 18:19):

Involves matching on a type, which is inconsistent?

#### Mario Carneiro (Oct 18 2020 at 18:20):

well for starters #eval doesn't work on real numbers

#### Mario Carneiro (Oct 18 2020 at 18:20):

also you are missing your prologue for the #mwe

#### Kevin Sullivan (Oct 18 2020 at 18:21):

The problem is in jack. Each of the s is read as being of type (typeForFoo f) not as the reduced value of that expression. Yes, ok, on the evals (deleted), and sorry about missing import of reals from mathlib.

#### Mario Carneiro (Oct 18 2020 at 18:24):

Because s depends on f, you have to match on them together

def jack (f : foo) (s : typeForFoo f) : bar :=
match f, s with
| foo.R, s := bar.mk s 0
| foo.N, s := bar.mk 0 s
end


#### Kevin Sullivan (Oct 18 2020 at 18:33):

Thank you, Mario.

Mario Carneiro said:

Because s depends on f, you have to match on them together

def jack (f : foo) (s : typeForFoo f) : bar :=
match f, s with
| foo.R, s := bar.mk s 0
| foo.N, s := bar.mk 0 s
end


Last updated: May 10 2021 at 18:22 UTC