From f93eaf36f6aac2c6767d1cb5afba797949252de8 Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Wed, 28 Aug 2024 21:20:24 +0200 Subject: [PATCH] Re-enable Search in the 2024 file fundamentals_lecture --- 2024-07-Minneapolis/2_Coq/fundamentals_lecture.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v index f5cb2a8..100a612 100644 --- a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v +++ b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v @@ -572,10 +572,10 @@ in UniMath it is very important to be able to search the library so that you don't do something someone else has already done. *) (** To find everything about nat type: *) -(* Search nat. *) +Search nat. (** To search for all lemmas involving the pattern *) -(* Search _ (_ -> _ -> _). *) +Search _ (_ -> _ -> _). (** To find information about a notation *) Locate "+".