converting Prop to Type

Stream: new members

[Jason Gross]

I'm getting a type mismatch error (in Lean 4, if that's relevant) saying that something has type Prop but is expected to have type Type. What's the correct way to convert? (Also, is there a way to discover this? #search (Prop → Type) just tells me that it expects a term, not search...)

[Adam Topaz]

In lean3 we have docs#plift

[Adam Topaz]

I'm not sure about lean4

[Jason Gross]

Thanks, copying that definition works fine for my purposes

[Floris van Doorn]

Lean 4 has PLift: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L199

[Jason Gross]

Awesome, thanks!

[Kevin Buzzard]

I'm serious -- this is one of my favourite definitions in Lean. Here's the Lean 4 version:

structure PLift (α : Sort u) : Type u where
  up :: (down : α)

What I like about it is that it defines up and down at the same time as defining PLift all in some really nice way.