# Zulip Chat Archive

## Stream: general

### Topic: if-in-Type

#### Scott Morrison (Jun 02 2021 at 00:02):

Is it plausible to extend the meaning of `if h : X then ... else ...`

so that `X`

doesn't need to be a `Prop`

, but could be in `Type*`

?

Everything would have exactly the usual meaning: in the "yes" branch, we'd have a term `h : X`

, and in the "no" branch we'd have a term `h : X → false`

.

We'd have to generalize away from `decidable_pred`

, but there's a perfectly sensible notion for arbitrary types, i.e. an algorithm that either produces an element or a proof of `X → false`

. In `classical`

mode this could still apply to every type.

I feel like we could avoid some beating around the bush with `nonempty`

sometimes if `if`

statements were allowed to go for the witness directly.

#### Mario Carneiro (Jun 02 2021 at 00:09):

I would prefer for this to be a separate definition, although I don't know if you can declare a notation like `if then else`

yourself in lean 3 - I think that one is implemented directly in C++

#### Mario Carneiro (Jun 02 2021 at 00:17):

```
@[class] inductive {u} choicy (α : Type u) : Type u
| pos : α → choicy
| neg : (α → false) → choicy
noncomputable instance classical.choicy (α) : choicy α :=
by classical; exact
if h : nonempty α then choicy.pos (classical.choice h) else choicy.neg (λ a, h ⟨a⟩)
def type_ite {C} (α : Type*) [d : choicy α] (t : α → C) (e : (α → false) → C) : C :=
choicy.rec_on d t e
```

I don't really know what kind of types would have nontrivial `choicy`

instances though

#### Mario Carneiro (Jun 02 2021 at 00:20):

maybe it would be better to simplify this to eliminate the `choicy`

class and just use this for your choicy ite needs:

```
noncomputable def choicy_ite {C} (α) (t : α → C) (e : (α → false) → C) : C :=
by classical; exact
if h : nonempty α then t (classical.choice h) else e (λ a, h ⟨a⟩)
```

#### Eric Wieser (Jun 02 2021 at 06:50):

I explored this a little before at https://gist.github.com/eric-wieser/103ad49e8c5c4415991b7622f77c48e0

#### Eric Wieser (Jun 02 2021 at 06:51):

Using psum is consistent with docs#classical.type_decidable

Last updated: Aug 03 2023 at 10:10 UTC