From c050ec21aef31960d761c1bded9512405963f9ae Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 9 Feb 2020 13:17:48 -0500 Subject: [PATCH] Proofreading FirstClassFunctions --- FirstClassFunctions.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FirstClassFunctions.v b/FirstClassFunctions.v index 418a575..0ab7d38 100644 --- a/FirstClassFunctions.v +++ b/FirstClassFunctions.v @@ -164,7 +164,7 @@ Fixpoint sorted {A} (le : A -> A -> bool) (ls : list A) : bool := end end. -(* [insert] preserves sortedness. Note the crucial hypothesis that comaprator +(* [insert] preserves sortedness. Note the crucial hypothesis that comparator * [le] is *total*: any two elements are related by it, in one order or the * other. *) Lemma insert_sorted : forall {A} (le : A -> A -> bool) a, @@ -189,7 +189,7 @@ Proof. rewrite H3, H4; trivial. rewrite H1; simplify. trivial. -Qed. +Qed. (* Main theorem: [insertion_sort] produces only sorted lists. *) Theorem insertion_sort_sorted : forall {A} (le : A -> A -> bool),