something is causing “unreachable code was reached” error

forked-from-1kasper · Dec 10, 2024 · 7a32006 · 7a32006
1 parent 1e6b516
commit 7a32006
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/GroundZero/Exercises/Chap4.lean b/GroundZero/Exercises/Chap4.lean
@@ -434,7 +434,7 @@ namespace «4.8»
   open GroundZero.Structures
   open GroundZero.Theorems
 
-  hott lemma injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
+  noncomputable hott lemma injOutOfBoolChar {B : Type u} : (Σ (f : 𝟐 → B), injective f) ≃ (Σ (w : B × B), w.1 ≠ w.2) :=
   begin
     fapply Sigma.mk;
     { intro w; existsi (w.1 false, w.1 true);
@@ -453,7 +453,7 @@ namespace «4.8»
       { apply Theorems.funext; intro b; induction b using Bool.casesOn <;> reflexivity } }
   end
 
-  hott lemma embdOutOfBoolChar {B : Type u} :
+  noncomputable hott lemma embdOutOfBoolChar {B : Type u} :
     (𝟐 ↪ B) ≃ (Σ (w : B × B), w.1 ≠ w.2 × contr (w.1 = w.1) × contr (w.2 = w.2)) :=
   begin
     fapply Sigma.mk;