Zulip Chat Archive

Stream: new members

Topic: converting Prop to Type


Jason Gross (Mar 05 2021 at 18:28):

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 (Mar 05 2021 at 18:31):

In lean3 we have docs#plift

Adam Topaz (Mar 05 2021 at 18:31):

I'm not sure about lean4

Jason Gross (Mar 05 2021 at 18:34):

Thanks, copying that definition works fine for my purposes

Floris van Doorn (Mar 05 2021 at 18:49):

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

Jason Gross (Mar 05 2021 at 18:49):

Awesome, thanks!

Kevin Buzzard (Mar 05 2021 at 19:33):

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.


Last updated: Dec 20 2023 at 11:08 UTC