## Stream: general

### Topic: set coe_to_sort constructor

#### Patrick Massot (Jun 18 2020 at 08:59):

What is the official name of def mk_it {α : Type*} {s : set α} {x : α} (h : x ∈ s) : s := ⟨x, h⟩? Surprisingly I need it in let statement, Lean simply doesn't let me define something of type s without this function.

#### Patrick Massot (Jun 18 2020 at 09:01):

And now I see cases tactic failed, unexpected failure when introducing auxiliary equatilies. I really need to learn stuff about that coercion from sets to types.

#### Rob Lewis (Jun 18 2020 at 09:02):

subtype.mk?

#### Patrick Massot (Jun 18 2020 at 09:14):

The question is: how to you make let believing that obvious answer?

example {α : Type*} {s : set α} (x :α) (h : x ∈ s) : true :=
begin
let X : s := subtype.mk x h, -- error!
sorry
end


#### Rob Lewis (Jun 18 2020 at 09:23):

let X : ↥s := subtype.mk x h? :(

#### Patrick Massot (Jun 18 2020 at 09:30):

Indeed that works, but doesn't make me feel super happy.

#### Mario Carneiro (Jun 18 2020 at 09:34):

We could fix it by using  t ← i_to_expr (%%e : Sort*) or the like in let, but I think that will produce a coe rather than a coe_sort

#### Mario Carneiro (Jun 18 2020 at 09:35):

I don't know if there is a function exposed that will allow us to trigger the coe-to-sort parser transform

#### Mario Carneiro (Jun 18 2020 at 09:36):

I suppose a hack would be to elaborate \lam (x : e), x and then extract e

#### Kevin Buzzard (Jun 18 2020 at 10:31):

Oh I see -- the issue is that lean will automatically insert a coe, but not a coe to sort?

#### Mario Carneiro (Jun 18 2020 at 10:33):

It will still typecheck, but it will be an observable difference and that could lead to downstream breakage

#### Mario Carneiro (Jun 18 2020 at 10:34):

for example if one has a simp lemma and the other doesn't

#### Mario Carneiro (Jun 18 2020 at 10:35):

As is it's not inserting any coe because the "type" is parsed first and then the value is parsed and asserted to have the type (which is okay because the type is coerced here) and then the type and the value are passed to definev which complains because the "type" isn't a type

#### Mario Carneiro (Jun 18 2020 at 10:36):

(This bug is in the code of tactic.interactive.let btw)

#### Yury G. Kudryashov (Jun 18 2020 at 12:14):

  let X : ↥s := ⟨x, h⟩, -- works


Last updated: May 09 2021 at 19:11 UTC