Zulip Chat Archive
Stream: general
Topic: Casting from Prop to Type u
Johan Commelin (Jul 31 2018 at 09:47):
I've got a prop P : Prop, but now I need to view P as a term of Type u. How do I cast/lift it like that?
Kenny Lau (Jul 31 2018 at 09:47):
plift
Chris Hughes (Jul 31 2018 at 09:48):
plift?
Johan Commelin (Jul 31 2018 at 09:48):
You're end bosses!
Last updated: Dec 20 2023 at 11:08 UTC