JamesGallicchio / LeanColls

WIP collections library for Lean 4
https://jamesgallicchio.github.io/LeanColls/docs/
Apache License 2.0
30 stars 7 forks source link

Naming arguments of Ops #1

Closed lecopivo closed 10 months ago

lecopivo commented 10 months ago

I would prefer if arguments of functions have (somewhat)meaningful names rather than being anonymous.

For example Fold would be defined as

class Fold (C : Type u) (τ : outParam (Type v)) where
  fold {β : Type w} (c : C) (f : β → τ → β) (init : β) : β
  foldM {β : Type w} {m : Type w → Type w} [Monad m]
      (c : C) (f : β → τ → m β) (init : β) : m β

Maybe even better would be following GetElem convention

class Fold (cont : Type u) (Elem : outParam (Type v)) where
  fold {β : Type w} (cont : Cont) (f : β → Elem → β) (init : β) : β
  foldM {β : Type w} {m : Type w → Type w} [Monad m]
      (cont : Cont) (f : β → Elem → m β) (init : β) : m β
JamesGallicchio commented 10 months ago

agreed. I like the GetElem convention with cont.