From a7c33a963fefef3225249e1fa313d13d44887b50 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Thu, 9 Jun 2022 15:38:48 -0400 Subject: [PATCH] doc: docstrings for List.isPrefixOf --- src/Init/Data/Array/Basic.lean | 3 ++- src/Init/Data/List/Basic.lean | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index bd14f8aa9c..31c19b58ea 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -765,7 +765,8 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N true termination_by _ => as.size - i -/- Return true iff `as` is a prefix of `bs` -/ +/-- Return true iff `as` is a prefix of `bs`. +That is, `bs = as ++ t` for some `t : List α`.-/ def isPrefixOf [BEq α] (as bs : Array α) : Bool := if h : as.size ≤ bs.size then isPrefixOfAux as bs h 0 diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index e14a7efdaa..1de7d3ad75 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -423,13 +423,15 @@ instance [LT α] : LE (List α) := ⟨List.le⟩ instance [LT α] [DecidableRel ((· < ·) : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := fun _ _ => inferInstanceAs (Decidable (Not _)) -/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/ +/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. +That is, there exists a `t` such that `l₂ == l₁ ++ t`. -/ def isPrefixOf [BEq α] : List α → List α → Bool | [], _ => true | _, [] => false | a::as, b::bs => a == b && isPrefixOf as bs -/-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/ +/-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. +That is, there exists a `t` such that `l₂ == t ++ l₁`. -/ def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool := isPrefixOf l₁.reverse l₂.reverse