elim ite

Stream: new members

[kana]

What is the best and simplest way to make it correct:

def f (x : bool) (y : if x then string else nat) : string :=
  if x then y else y.to_string

[Eric Wieser]

This works:

def nat.to_string (n : ℕ) : string := sorry

def f : ∀ (x : bool) (y : if x then string else nat), string
| tt y := y
| ff y := y.to_string

What do I import to get docs#nat.to_string?

[kana]

Thanks. Sorry, should be just to_string y

[Yakov Pechersky]

No, that won't work either.

[Yakov Pechersky]

(also, use cond instead of ite when working with bool)

[Eric Wieser]

docs#to_string?

[Eric Wieser]

def f : ∀ (x : bool) (y : if x then string else nat), string
| tt y := y
| ff y := to_string (show ℕ, from y)

[Yakov Pechersky]

Why not just use string ⊕ nat instead of the pi type over bool?