Nicer counter-example

Lean4CheckerTests/OverridenPrelude.lean

@@ -2,21 +2,22 @@ prelude
 
 set_option autoImplicit false
 
-universe u
-variable {α : Type u}
-
-inductive Eq : α → α → Prop where
-  | refl (a : α) : Eq a a
-
 inductive Nat where
   | zero : Nat
   | succ (n : Nat) : Nat
 
 -- The kernel has a hard-coded interpretation for this function
+-- which differs from the one we give here
 def Nat.add : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero
--- But not this function
-def Nat.add2 : (@& Nat) → (@& Nat) → Nat := fun _ _ => .succ .zero
 
-theorem eq1 (x : Nat ): Eq (Nat.add x Nat.zero) (Nat.add2 x Nat.zero) := Eq.refl _
-theorem eq2 : Eq (Nat.add .zero .zero) (Nat.add2 .zero .zero) := eq1 _
-theorem eq3 : Eq (Nat.zero) (.succ .zero) := eq2
+inductive Empty : Type
+structure Unit : Type
+
+def T (n : Nat) : Type :=
+  Nat.rec Empty (fun _ _ => Unit) n
+
+def test (n : Nat) : T (Nat.add n .zero) := Unit.mk
+def test0 : T (Nat.add .zero .zero) := test .zero
+def empty : Empty := test0
+
+theorem boom (P : Prop) : P := Empty.rec empty

test.sh

@@ -1,12 +1,6 @@
 #!/usr/bin/env bash
 
-<<<<<<< HEAD
 lake build
-=======
-# Because `Lean4CheckerTests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-# we just keep rebuilding until it works!
-until lake build > /dev/null 2>&1; do :; done
->>>>>>> 8a73e92 (Add a test case about overriding the prelude)
 
 check_command() {
     local cmd="$1"