Zulip Chat Archive
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 onf
, you have to match on them togetherdef 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: Dec 20 2023 at 11:08 UTC