Re-enable instances of Search in the 2024 directory

2024-07-Minneapolis/4_Tactics/tactics_lecture.v

@@ -42,9 +42,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  (* Search bool. *)
+  Search bool.
   (** If you only want to find library elements that *yield* booleans, then try *)
-  (* SearchPattern bool. *)
+  SearchPattern bool.
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -56,15 +56,15 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-(* Search bool. *)
+Search bool.
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
 
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -97,7 +97,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -384,7 +384,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    (* SearchPattern (_ × _ =  _ × _). *)
+    SearchPattern (_ × _ =  _ × _).
     (** Nothing for our equation - we can only hope for weak equivalence ≃,
         see the exercises. *)
 Abort.

2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v

@@ -49,9 +49,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  (* Search bool. *)
+  Search bool.
   (** If you only want to find library elements that *yield* booleans, then try *)
-  (* SearchPattern bool. *)
+  SearchPattern bool.
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -65,7 +65,7 @@ Defined.
     verify it and to associate it with the given identifer, here [myfirsttruthvalue].
     This may go wrong for different reasons, including implementation errors of the Coq
     system - that will not affect trustworthiness of the library. *)
-(* Search bool. *)
+Search bool.
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -76,7 +76,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -109,7 +109,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -359,7 +359,7 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-(* SearchPattern (paths _ _). *)
+SearchPattern (paths _ _).
 (** Among the search results is [pathsinv0r] that has [idpath] in its conclusion. *)
 (* SearchRewrite idpath. *)
 (** No result! *)
@@ -496,11 +496,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    (* SearchPattern (_ × _ =  _ × _). *)
+    SearchPattern (_ × _ =  _ × _).
     (** Nothing for our equation - we can only hope for weak equivalence ≃. *)
 Abort.
 
-(* SearchPattern(_ ≃ _). *)
+SearchPattern(_ ≃ _).
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.

2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v

@@ -194,7 +194,7 @@ Admitted.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
+  + Search ( (_ = _) ≃ ( _ ≃ _)).
     (* Solve this goal. *)
     admit.
   + (* Solve this goal. *)
@@ -277,7 +277,7 @@ Proof.
   unfold monoidiso'.
   unfold monoidiso.
   (* Observe that this is just an reassociation of Sigma-types. *)
-  (* Search ( (∑ _ , _ ) ≃ _ ). *)
+  Search ( (∑ _ , _ ) ≃ _ ).
   admit.
 Admitted.
 

2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v

@@ -217,7 +217,7 @@ Defined.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
+  + Search ( (_ = _) ≃ ( _ ≃ _)).
     use hSet_univalence.
   + intro p.
     induction X as [X x].
@@ -257,7 +257,7 @@ Local Open Scope multmonoid.
 Notation "x * y" := (op x y) : multmonoid.
 Notation "1" := (unel _) : multmonoid.
 
-(* Search monoid. *)
+Search monoid.
 
 (*
   Construct the following chain of equivalences

2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v

@@ -311,7 +311,7 @@ Section Exercise_2.
     : is_univalent pointed_operation_set.
   Proof.
     apply is_univalent_total_category.
-    - (* Search HSET. *)
+    - Search HSET.
       exact is_univalent_HSET.
     - exact pointed_operation_is_univalent_disp.
   Defined.