From 254e2aedc6ea7de2bd2c29440d03762ef8be0911 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 23 Feb 2020 16:20:39 -0500 Subject: [PATCH] Tiny copy-editing --- DataAbstraction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DataAbstraction.v b/DataAbstraction.v index f4b0e09..6616a2a 100644 --- a/DataAbstraction.v +++ b/DataAbstraction.v @@ -150,7 +150,7 @@ Module Algebraic. Definition empty A : t A := []. Definition enqueue A (q : t A) (x : A) : t A := q ++ [x]. - (* [dequeue] is now constant time, with no recursion and just a single + (* [dequeue] is now constant-time, with no recursion and just a single * pattern match. *) Definition dequeue A (q : t A) : option (t A * A) := match q with