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):
Chris Hughes (Jul 31 2018 at 09:48):
Johan Commelin (Jul 31 2018 at 09:48):
You're end bosses!
Last updated: Aug 03 2023 at 10:10 UTC