feat: add PEmpty

closes #537
leanprover · Aug 7, 2021 · 8a84532 · 8a84532
1 parent 6e2b718
commit 8a84532
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 5 deletions.
diff --git a/src/Init/Prelude.lean b/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 :=

diff --git a/tests/lean/276.lean b/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 _ => α)

diff --git a/tests/lean/276.lean.expected.out b/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