lens combinator?

[quinn-dougherty]

Does it make sense to provide this combinator or does the MetaCoq aspect give us equivalent functionality?

Should be

Definition lens {a b c d : Type} (ac : a -> c) (adb : a -> d -> b) : Lens a b c d :=
  {| view := ac; over := fun (f : c -> d) (x : a) => adb x (f (ac x)) |}.

[gmalecha]

This combinator makes sense, but it isn't the best implementation in a lot of cases because you will destruct x multiple times. For inductive types and such, what coq-elpi generates should be more efficient.