fix(library,hott): comment 'exit' commands to avoid warnings during compilation

hott/types/W.hlean

@@ -12,6 +12,7 @@ import .sigma .pi
 open eq sigma sigma.ops equiv is_equiv
 
 -- TODO fix universe levels
+/-
 exit
 
 inductive Wtype.{l k} {A : Type.{l}} (B : A → Type.{k}) :=
@@ -155,3 +156,4 @@ namespace Wtype
   end
 
 end Wtype
+-/

library/logic/examples/instances_test.lean

@@ -21,6 +21,7 @@ set_option class.conservative false
 example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 subst iff H1 H2
 
+/-
 exit
 example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 H1 ▸ H2
@@ -39,3 +40,4 @@ H1 ⬝ H2⁻¹ ⬝ H3
 
 example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
 H1 ⬝ H2⁻¹ ⬝ H3
+-/