Zulip Chat Archive

Stream: new members

Topic: elim ite


view this post on Zulip kana (Mar 02 2021 at 15:00):

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

view this post on Zulip Eric Wieser (Mar 02 2021 at 15:03):

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?

view this post on Zulip kana (Mar 02 2021 at 15:04):

Thanks. Sorry, should be just to_string y

view this post on Zulip Yakov Pechersky (Mar 02 2021 at 15:06):

No, that won't work either.

view this post on Zulip Yakov Pechersky (Mar 02 2021 at 15:07):

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

view this post on Zulip Eric Wieser (Mar 02 2021 at 15:08):

docs#to_string?

view this post on Zulip Eric Wieser (Mar 02 2021 at 15:10):

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

view this post on Zulip Yakov Pechersky (Mar 02 2021 at 15:13):

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


Last updated: May 17 2021 at 21:12 UTC