Zulip Chat Archive

Stream: lean4

Topic: Naming for list lemmas


James Gallicchio (Aug 24 2022 at 18:23):

Hey, just lookin for some thoughts about what to call various lemmas :)

  theorem foldl_cons (L : List τ) (acc)
    : L.foldl (fun acc x => x :: acc) acc = L.reverseAux acc
    := by sorry

  theorem foldl_append (L : List τ) (acc : β)
    : L.foldl (fun acc x => acc ++ [x]) = L
    := by sorry

  theorem map_eq_foldl (L : List τ) (f) (acc : β)
    : L.map f = L.foldl (fun acc x => acc ++ [f x])
    := by sorry

  theorem foldl_of_append (L₁ L₂ : List τ) (f) (acc : β)
    : (L₁ ++ L₂).foldl f acc = L₂.foldl f (L₁.foldl f acc)
    := by sorry

There's a bunch of these types of lemmas I'm writing, not really sure how to organize them


Last updated: Dec 20 2023 at 11:08 UTC