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