feat: add PEmpty

closes #537

src/Init/Prelude.lean

@@ -47,6 +47,9 @@ inductive False : Prop
 
 inductive Empty : Type
 
+set_option bootstrap.inductiveCheckResultingUniverse false in
+inductive PEmpty : Sort u where
+
 def Not (a : Prop) : Prop := a → False
 
 @[macroInline] def False.elim {C : Sort u} (h : False) : C :=

tests/lean/276.lean

@@ -1,9 +1,5 @@
 universe u v
 
--- `Type u` version can be defined without this option, but I get the same error
-set_option bootstrap.inductiveCheckResultingUniverse false in
-inductive PEmpty : Sort u
-
 -- `#check` works
 set_option pp.all true in
 #check fun {α : Sort v} => PEmpty.rec (fun _ => α)

tests/lean/276.lean.expected.out

@@ -1,2 +1,2 @@
 fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
-276.lean:13:4-13:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion
+276.lean:9:4-9:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion