set coe_to_sort constructor

Stream: general

[Patrick Massot]

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]

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]

subtype.mk?

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Yury G. Kudryashov]

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